Prelude

Prelude is a built-in module, containing several definitions, which behave differently from ordinary definitions. It is always imported implicitly in every module. You can also import it explicitly to hide or rename some of its definitions.

We will discuss these definitions in this module. You can look at the file Prelude.ard, which contains these definitions, but note that they only roughly correspond to actual definitions since most of them cannot be actually defined in the ordinary syntax.

Nat and Int

The definitions of Nat, Int, Nat.*, Nat.<=, and Nat.div are actually correct, they could have been as well defined in an ordinary file and successfully typechecked according to normal Arend typechecking rules. The only difference is that these definitions from Prelude are implemented more efficiently. Definitions of Nat.divMod, Nat.divModProp, and Nat.modProp are omitted, but these functions also can be defined in Arend.

Functions Nat.+ and Nat.- have more computational rules than can be defined normally:

n + 0 => n
n + suc m => suc (n + m)
0 + m => m
suc n + m => suc (n + m)

0 - m => neg m
n - 0 => pos n
suc n - suc m => n - m

Finally, Nat.mod (suc n) has type Fin (suc n) and Nat.divMod (suc n) has type \Sigma Nat (Fin (suc n)).

Fin

The type Fin n is a subtype of Nat and also a subtype of Fin (suc n). Constructors of Nat are also constructors of Fin n: zero has type Fin (suc n) and if x : Fin n, then suc x : Fin (suc n).

Array

Array is a record consisting of a type of its elements A, its length len, and a function Fin len -> A. Thus, Array A is equivalent to the type of lists of elements of type A and Array A n is equivalent to the type of vectors of elements of type A and length n.

The prelude also includes constructors nil and :: which can be used to define functions on arrays by pattern matching. Thus, arrays can be used as functions Fin len -> A and as lists simultaneously.

The type of dependent arrays DArray is a generalization of Array in which A : Fin len -> \Type is a dependent type and elements are given by a dependent function \Pi (j : Fin len) -> A j.

Interval and squeeze functions

The definition of the interval type \data I | left | right looks like the definition of the set with two elements, but this is not true actually. One way to think about this data type is that it has one more constructor, which connects left and right and which cannot be accessed explicitly. This means that it is forbidden to define a function on I by pattern matching. Functions from I can be defined by means of several auxiliary functions: coe, coe2, squeeze, squeezeR. Function coe plays the role of eliminator for I, it is discussed further in this module.

Functions squeeze and squeezeR satisfy the following computational conditions:

squeeze left j => left
squeeze right j => j
squeeze i left => left
squeeze i right => i

squeezeR left j => j
squeezeR right j => right
squeezeR i left => i
squeezeR i right => right

Such functions can be defined in terms of the function coe, but for efficiency purposes they are defined as primitives in Arend.

Path

The definition of Path A a a’ is not correct. By the definition, it should consist of all functions \Pi (i : I) -> A i, but actually it consists of all such functions f that also satisfy computational conditions f left => a and f right => a’. This means that while typechecking the expression path f the typechecker also checks that these computational conditions hold and, if they don’t, produces an error message. For example, if you write \func test : 1 = 0 => path (\lam _ => 0), you will see the following error message:

[ERROR] test.ard:1:23: The left path endpoint mismatch
  Expected: 1
    Actual: 0
  In: path (\lam _ => 0)
  While processing: test

The homotopy level of the universe, which is the type of Path, is also computed differently. If -1 ≤ n and A is in a universe of (n+1)-types, then Path A a a’ is in a universe of n-types. Otherwise, it has the same homotopy level as A.

Prelude also contains an infix form of Path called = which is actually a correctly defined function. The definition of @ is also correct, but the typechecker has an eta rule for this definition:

path (\lam i => p @ i) == p

This rule does not apply to functions @ defined in other files.

There is also an implicit coercion between paths and functions of type \Pi (i : I) -> A i. That is, when such a function occurs in a place where a path is expected, path is automatically inserted. The converse is also true: paths are automatically converted to such functions with @.

Path.inProp

The function Path.inProp is not correct since it does not have a body. It postulates the proof irrelevance for types in \Prop, namely that any two elements of a type in \Prop are equal.

idp

The constructor idp is not a correct definition since it is not allowed to use lambdas in constructors. This constructor can be used to replace the J operator with pattern matching. For example, we can define J itself as follows:

\func J {A : \Type} {a : A} (B : \Pi (a' : A) -> a = a' -> \Type) (b : B a idp) {a' : A} (p : a = a') : B a' p \elim p
  | idp => b

After we match p with idp, variables a and a’ become equivalent. To be more precise, we can refer to both variables, but the latter will evaluate to the former.

There are certain restrictions on this pattern matching principle. If we want to match p : e = e’ with idp, expressions e and e’ cannot be arbitrary. At least one of them must be a variable which does not occur in the other expression. Also, it should be possible to substitute the variable with this expression, which means that the free variables of the expression should be bound at each occurrence of the variable.

This pattern matching principle can also be used in case-expressions. For example, J can be defined as follows:

\func J {A : \Type} {a : A} (B : \Pi (a' : A) -> a = a' -> \Type) (b : B a idp) {a' : A} (p : a = a') : B a' p
  => \case \elim a', \elim p \with {
    | _, idp => b
  }

Note that the restrictions we described above should be satisfied. Moreover, the expression which is matched with idp should have type p : e = e’, where either e or e’ is a variable bound in one of the arguments of the case expression.

coe and coe2

Function coe is an eliminator for the interval type. For every type over the interval, it allows to transport elements from the fiber over left to the fiber over an arbitrary point. It can be used to prove that I is contractible and that = satisfies the rules for ordinary identity types. The definition of coe is not correct since it uses pattern matching on the interval. This function satisfies one additional reduction rule:

coe (\lam x => A) a i => a

if x is not free in A.

Function coe2 is a generalization of coe, which allows to transport elements between any two fibers of a type over the interval.

iso

The definition of iso is not correct since it uses pattern matching on the interval. This definition implies the univalence axiom.