```
{-# OPTIONS --cubical #-}
open import SomeStuff
module notes where
```
Homotopy type theory for programmers
====================================
This is how we can define data types in agda:
```
data Bool : Set where
true : Bool
false : Bool
data Empty : Set where
```
Think of `true` and `false` as constructors of the data type `Bool`.
As everything here is immutable/const, the only values of type `Bool` are those we can construct with a constructor.
This means, to define a function, it is enough to say, what it does for values constructed with a constructor-call:
```
negation : Bool -> Bool -- declaration
negation true = false -- definition for true
negation false = true -- definition for false
```
Constructors can have arguments:
```
data 2Bit : Set where
bits : Bool -> Bool -> 2Bit
-- (↑ this is a two argument function!)
-- 'same as' (Bool × Bool) -> 2Bit
someBits = bits true false
```
Data types can have type parameters:
```
-- (↓ 'A' is some type)
data Maybe (A : Set) : Set where
just : A → Maybe A
nothing : Maybe A
```
Just to see one more example of a function definition:
(Using a type `A` as argument...)
```
getWithDefault : {A : Set} -> A -> Maybe A -> A
getWithDefault x (just y) = y
getWithDefault x nothing = x
```
This is a must for any tutorial on inductive data types and a good test for your understanding:
```
data ℕ : Set where
zero : ℕ
1+ : ℕ -> ℕ -- also known as 'succ'
one = 1+ zero
```
Some examples of functions:
```
plus : ℕ -> ℕ -> ℕ
plus zero y = y
plus (1+ x) y = 1+ (plus x y)
{- same thing, more intense notation:
↓ ↓ places for arguments can be marked with '_' -}
_+_ : ℕ → ℕ → ℕ
zero + y = y
(1+ x) + y = 1+ (x + y)
```
Now an example where we vary the `: Set`, an inductive family:
```
data Vector (A : Set) : ℕ → Set where
[] : Vector A zero
_∷_ : {n : ℕ} → A → Vector A n → Vector A (1+ n)
append : {A : Set} {n m : ℕ} → Vector A n → Vector A m → Vector A (n + m)
append [] v = v
append (x ∷ v) u = x ∷ (append v u)
{-
append' : {A : Set} {n m : ℕ} → Vector A n → Vector A m → Vector A (m + n)
append' [] v = v
append' (x ∷ v) u = x ∷ (append v u)
-}
```
Equality in (Martin-Löf) dependent type theory can be *defined* as an inductive data type (this is a bit of a hack... but in the end it is some type with the correct behaviour):
```
data Equal (A : Set) : A -> A -> Set where
reflexivity : (x : A) -> Equal A x x
```
(simplify notation?)
```
data _==_ {A : Set} : A -> A -> Set where
refl : (x : A) -> _==_ x x
comm : (x y : ℕ) -> (x + y) == (y + x)
comm = {!!}
```
We can express some properties of equality by defining functions...
```
symmetric : {A : Set} {x y : A} → x == y → y == x
symmetric (refl x) = refl x
transitive : {A : Set} {x y z : A} → x == y → y == z → x == z
transitive (refl _) q = q
```
But this turns out to be way more usefull and general: It also works
if we think of 'equality' as 'path' in a space (this can be made precise).
A surface between two paths can be thought of as an equality of equalities then.
So we can 'symmetric' and 'transitive' as operations on paths:
(pictures)
```
_∙_ : {A : Set} {x y z : A} → x == y → y == z → x == z
(refl _) ∙ q = q
_⁻¹ : {A : Set} {x y : A} → x == y → y == x
(refl _)⁻¹ = refl _
```
Back to data types.
Elements 'constructorₗ x₁ ... xₙ' 'constructorₖ y₁ ... yₘ'
of a 'data' type are equal
if and only if
l == k
and xᵢ == yᵢ for all valid i
Is '_==_' always 'the correct' equality?
```
data Name : Set where
name : String -> Name
```
Maybe we want 'name "Felix" == name "felix"'...
An example from math:
We can define ℤ as the type of pairs (a,b) with a,b:ℕ and think of (a,b) as the integer b-a. So we need (a,b)==(c,d) <=> b-a == d-c <=> b+c == d+a.
Appraoch 1: Normal forms
For the names, we can ask for normalized strings.
For ℤ, we can use two copies of ℕ and a new zero:
```
data ℤ : Set where
pos+1 : ℕ → ℤ
zero : ℤ
neg-1 : ℕ → ℤ
```
Apporach 2: Higher inductive types
Use the cubical path/equality type and just add 'higher constructors':
```
data ℤ-HIT : Set where
_,_ : ℕ → ℕ → ℤ-HIT
diff-eq : (a b c d : ℕ) → (b + c) ≡ (d + a) → (a , b) ≡ (c , d)
-- ↑ this is the cubical equality...
```
It is possible to show that ℤ and ℤ-HIT 'are the same type' up to equalities between equalities...
So there are some equalities we never explicitly asked for....
Let's say we want a quotient - let us start with the simplest possible example:
```
data Trivial : Set where
t : Trivial
p : t ≡ t
```
A function 'f : Trivial → B' can be defined by cases for:
f t =
'f p' =...
If there is a type X with p : x == x such that p is different from refl, we can show p is different from refl.
And then,
'Trivial' is not at all trivial and known as the (homotopical) circle or S¹:
```
data S¹ : Set where
base : S¹
loop : base ≡ base
```
```
d : S¹' → S¹
d = S¹-rec base (loop ∙₂ loop)
```
One can show in cubical agda: (base ≡ base) is ℤ.
"Because": p and p ∙ p have to be different,
also p ⁻¹ and p
Can we understand the type S¹ completely?
Yes, in the case of S¹, absolutely not in the case of S²:
```
data Suspension (A : Set) : Set where
N : Suspension A
S : Suspension A
meridian : (x : A) → N ≡ S
S² = Suspension S¹
```