Tutorial

Arend language is based on homotopy type theory. For that reason, the most natural explanation for many language constructs in Arend, including the very basic ones, would be in terms of notions from homotopy theory. However, it is also possible to abstract away from homotopical semantics and to consider the layer of Arend that corresponds simply to a variant of the classical Martin-Löf dependent type theory. The latter view is taken in this tutorial for the initial exposition of the language in Part I, whereas homotopical semantics together with some specific for this semantics elements of the language are discussed in Part II.

The Part I is an introduction to the actual practices of working with dependent types in Arend. It contains example-based Arend-specific exposition of efficient ways of working with propositions and proofs, inductive types, classes and records, type universes, etc. We assume that the reader is familiar with basic concepts from ML-like languages (such as Haskell, Agda, or Coq/Gallina).

The Part II is a practical introduction to homotopy type theory in the context of Arend. Themes discussed here include data types with conditions (higher inductive types) and homotopy levels of universes.

The Arend code for the tutorial, including exercises, can be downloaded from here.