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

Here we look at its functions related to HoTT:

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

 ```\data Path (A : I -> \Type) (a : A left) (a' : A right) | path (\Pi (i : I) -> A i) \where { \lemma inProp {A : \Prop} : \Pi (a a' : A) -> a = a' }```

### Equality

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

` `
 ```\func \infix 1 = {A : \Type} (a a' : A) => Path (\lam _ => A) a a'```

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

 ``` \cons idp {A : \Type} {a : A} => path (\lam _ => a) ```

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

 ``` \func \infixl 9 @ {A : I -> \Type} {a : A left} {a' : A right} (p : Path A a a') (i : I) : A i \elim p, i | path f, i => f i | _, left => a | _, right => a' ```

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

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 iso {A B : \Type} (f : A -> B) (g : B -> A) (p : \Pi (x : A) -> g (f x) = x) (q : \Pi (y : B) -> f (g y) = y) (i : I) : \Type \elim i | left => A | right => B```

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.