Maths - HoTT in Arend

Arend is a computer language which has support for homotopy type theory (HoTT) and Cubical type theory.

More on the page here.

• Arend home
• Arend tutorial
• Arend code on github

Interval Type

This is not really a valid type but it can be appoximated by:

\data I | left | right

which looks like the definition of the set with two elements, but there is additional funtionality which is not defined here. One way to think about this 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.

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.

We are not allowed to define a function on I by pattern matching so this code is not strictly correct but it gives useful intuition.

\data I
  | left
  | right
  \where {
    \func squeeze (i j : I) : I
      | left, j => left
      | right, j => j
      | i, left => left
      | i, right => i

    \func squeezeR (i j : I) : I
      | left, j => j
      | right, j => right
      | i, left => i
      | i, right => right
  }

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.

Equality

The Arand prelude contains an infix form of Path called =.

idp

idp is the constructor for equalities. It is like Refl (short for reflexivity) in the language Idris for example

idp : a = a

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.

@ (at)

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 @.

coe

Function coe is an eliminator for the interval type.

For every type over the interval, it transports 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. 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.

We are not allowed to do pattern matching on the interval so this code is not strictly correct but it is a useful appoximation.

\func coe (A : I -> \Type)
          (a : A left)
          (i : I) :
                A i \elim i
  | left => a

\func coe2 (A : I -> \Type)
          (i : I) (a : A i)
          (j : I) : A j \elim i, j
  | left, j => coe A a j
  | i, right => coe
        (\lam k => A (I.squeezeR i k))
        a right

Isomorphism (iso function)

if f : A -> B is a “bijection” between types, namely, it satisfies isBij where \Set replaced with \Type, then the types A and B correspond to homotopy equivalent spaces and f is an equivalence. The function iso allows to construct a path between such spaces and the univalence says that the type of equivalences between types is equivalent to the type of paths between the types.