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