HoTT is a foundation for mathematics based on MLTT. In HoTT we don’t have sets like in ZFC, but elements of types.

A is a type and x : A is an element of type A.

data A : Type where
  a : A

Pi Types / Dependent function types

id : A -> A
id a = a

What we need

• an agda installation
• a nice text editor (Neovim + Cornelis)
• literate programming support

Working with Cornelis

We will assume two Types A and B.

data A : Type where
  a1 : A
  a2 : A

postulate
  B : Type

Load agda files with :CornelisLoad

Goals {!!}, :CornelisTypeContextInfer

someFunc : A -> B
someFunc a = {!!}

Split cases with :CornelisMakeCase.

-- switch : A -> A
-- switch a1 = a2
-- switch a2 = a1

switch : A -> A
switch a1 = a2
switch a2 = a1

What is switch a1? Normalize expressions with :CornelisNormalize

Links

• agda documentation: agda.readthedocs.io/en/v2.8.0
• nvim documentation: neovim.io/doc
• cornelis plugin: github.com/agda/cornelis

module 0Trinitarianism.Quest1 where
open import 0Trinitarianism.Preambles.P1

Predicates / Dependent Constructions / Bundles

isEven : ℕ → Type
isEven zero = ⊤  
isEven (suc zero) = ⊥
isEven (suc (suc n)) = isEven n

module 0Trinitarianism.Quest2 where

open import 0Trinitarianism.Preambles.P2

isEven : ℕ → Type
isEven zero = ⊤
isEven (suc zero) = ⊥
isEven (suc (suc n)) = isEven n

-- there exists an even natural number
existsEven : Σ ℕ isEven 
existsEven = zero , tt


_×_ : Type → Type → Type
A × C = Σ A (λ a → C)

div2 : Σ ℕ isEven → ℕ
div2 (zero , even) = 0
div2 (suc (suc n) , even_n) = suc ( div2 (n , even_n))

** A Tautology / Currying / Cartesian Closed **

private
  postulate
    A B C : Type


uncurry : (A → B → C) → (A × B → C)
uncurry f (a , b) = f a b

curry : (A × B → C) → (A → B → C)
curry f a b = f (a , b)

module 0Trinitarianism.Quest3 where

open import 0Trinitarianism.Preambles.P3

Defining Addition

We can define addition of natural numbers by induction on one of the arguments. This yields two defitions for addition.

_+_ : ℕ → ℕ → ℕ
zero + m   = m
suc n + m = suc (n + m)

_+'_ : ℕ → ℕ → ℕ
n +' zero = n
n +' suc m = suc (n +' m)

Sum of even natural numbers

Using the definition _+_ for addition it is easiest to do induction on the first argument it is easiest to do induction on x.

sumEven : ( x y : Σ ℕ isEven) -> isEven (x .fst + y .fst)
sumEven (zero , hx) y = y .snd
sumEven (suc (suc x) , hx) y = sumEven (x , hx ) y

Analogously we can do induction on y since _+'_ is defined by induction on the second argument.

sumEven' : ( x y : Σ ℕ isEven) -> isEven (x .fst +' y .fst)
sumEven' x (zero , hy) = x .snd
sumEven' x (suc (suc y) , hy) = sumEven' x (y , hy )

(Interestingly the second proof gets accepted for _+_ too.)

module 0Trinitarianism.Quest4 where
open import 0Trinitarianism.Preambles.P4

The Identity Type

We will view elements of Id as identifications / equalities.

Id denotes the identity type. We give a proof rfl for Id x x. In other words – Id is reflexive.

data Id {A : Type} : (x y : A) -> Type where
  rfl : {x : A} -> Id x x

Since rfl is the only element of type Id it suffices to show that rfl is symmetric. We do this by casing on p : Id which only allows rfl thus judgementally equal x and y.

idSym : (A : Type) (x y : A) -> Id x y -> Id y x
idSym A x y rfl = rfl

Or implicitly (what we will use from now on).

Sym : {A : Type} {x y : A} → Id x y → Id y x
Sym rfl = rfl

We can concatenate identifications to get results about transitivity.

idTrans : (A : Type) (x y z : A) -> Id x y -> Id y z -> Id x z
idTrans A x y z rfl rfl = rfl

Implicit concatenation

_*_ : {A : Type} {x y z : A}  -> Id x y -> Id y z -> Id x z
rfl * p = p

Groupoid Laws

Concatenation is right neutral.

rfl* : {A : Type} {x y : A} (p : Id x y) → Id (rfl * p) p
rfl* p = rfl

Concatenation with rfl is left neutral.

*rfl : {A : Type} {x y : A} (p : Id x y) → Id (p * rfl) p
*rfl rfl = rfl

Concatenation Sym p with p on the left and right gives rfl. In that sense Sym p can be interpreted as the “inverse” of p.

Sym* : {A : Type} {x y : A} (p : Id x y) → Id (Sym p * p) rfl
Sym* rfl = rfl

*Sym : {A : Type} {x y : A} (p : Id x y) → Id (p * Sym p) rfl
*Sym rfl = rfl

Concatenation is associative.

Assoc : {A : Type} {w x y z : A} (p : Id w x) (q : Id x y) (r : Id y z)
        → Id ((p * q) * r) (p * (q * r))
Assoc rfl q r = rfl

Agda uses its own type theory that is not HoTT.

Specifically the K-Rule is incompabtible with Homotopy Type Theory. Adding {-# OPTIONS --with-K #-} disables it.

Cubical Agda impelemts a different type theory that pairs more nicely with HoTT.