```agda
{-# OPTIONS --cubical #-}
open import SomeStuff
module notes where
```

Homotopy type theory for programmers
====================================

This is how we can define data types in agda:

```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:

```agda
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

```

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
```

p ∙ p is not p

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)
```
d base = base
d loop = 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¹
```