# Homotopy Type Theory  ## Homotopy  $f, g : X → Y, H : X × [0, 1] → Y → H(x, 0) = f(x), H(x, 1) = g(x).$$p : x =_A y.$$p, q : x =_A y.$

2-path/homotopy

r:p=x=Ayq.

## Types Are Higher Groupoids

### inverse : =-symmetry

First proof.

$λ(A).λ(a).λ(b).λ(p).ind=A(λ(a).λ(b).λ(p).(a = b), λa.refla, a, b, p) : (A : U) → (a, b : A) → (a = b) → (b = a).$

### concatenate/compose : =-transitivity

$λA.λa.λb.λc.λp.λq.ind=A(λa.λb.λp.λc.λq.(a = c), ind=A(λa.λc.λq.(a = c), refla)) : (A : U) → (a, b, c : A) → (a = b) → (b = c) → (a = c).$

### Lemma

A : U → x, y, z, w : A → p : x = y, q : y = z, r : z = w → 1. p = p ⋅ ↺_y, p = ↺_x ⋅ p. 2. p^[−1] ⋅ p = ↺_y, p ⋅ p^[−1] = ↺_x. 3. (p^[−1])^[−1] = p. 4. p ⋅ (q ⋅ r) = (p ⋅ q) ⋅ r.

### Eckmann–Hilton

$α, β : Ω^2(A, a) → α ⋅ β = β ⋅ α.$

### Pointed type

$(A, a) : U_• ≡ (A : U, A).$

### Loop space

$Ω(A, a) ≡ (a =_A a, ↺_a). Ω^0(A, a) ≡ (A, a), Ω^[n + 1](A, a) ≡ Ω^n(Ω(A, a)). Ω^2(A, a) ≡ Ω(Ω(A, a))≡ Ω((a =_A a, ↺_a)). ≡ Ω(a =_A a, ↺_a)≡ (↺_a =_[a =_A a] ↺_a, ↺_[↺_a]).$

## Functions Are Functors

### Lemma

$f : A → B, x, y : A → ap_f : (x =_A y) → (f(x) =_B f(y)). D ≡ (x, y, p) ↦ f(x) = f(y), D : x, y : A → (x = y) → U, d ≡ x ↦ ↺_[f(x)], d : x : A → D(x, x, ↺_x), ap_f : x, y : A → (x = y) → (f(x) = f(y)) (by path induction). x : A → ap_f(↺_x) ≡ ↺_[f(x)] (by computation rule).$



## Dependent Types are Fibrations

### Transport

#### Transport

$a : A → P : U → p : x =_A y → p_* ≡ transport^P(p, –) ≡ ind_[=_A](D, d, x, y, p) : P(x) → P(y), D ≡ x, y : A, p : x =_A y → P(x) = P(y), d ≡ x : A → id_[P(x)], ind_=_A(D, d, x, y, p) : P(x) → P(y) for p : x = y.$

Type theory: P respects equality: x = y → P(x) ≃ P(y). Topology: path lifting in a fibration P with base space A, with P(x) being the fibre over x and with Σ_[x : A] P being the total space of the fibration, with the first projection Σ_[x : A] P(x) → A.

#### Path lifting property

$A : U → a : A → P : U, a_0 : A, p_0 : P → p : x =_A y → lift(p_0, p) : (x, p_0) = (y, p_*(p_0)), pr_1(lift(p_0, p)) = p.$

#### Dependent map

$a : A → p : P → p : x =_A y → p_*(f(x)) =_[P(y)] f(y). D ≡ x, y, p →.(↺_x)_*(f(x)) ≡ f(x), d ≡ x : A → ↺_[f(x)],$

#### Lemma

$(f(x) = f(y)) → (p_*(f(x)) = f(y)),(p_*(f(x)) = f(y)) → (f(x) = f(y)).$



#### Lemma

$a : A → P : U, p : x =_A y, q : y =_A z, p_0 : P(x) → q_*(p_*(p_0)) = (p q)_*(p_0).$

#### Lemma

$a : A → b : B, b : B → P : U, p : x =_A y, p_0 : P(b(x)) →$

#### Lemma

$a : A → P, Q : U, (a : A → P → Q), p : x =_A y, p_0 : P(b(x)) →$

## Homotopies and Equivalences

### Homotopies

Natural transformations.

$f, g : (a : A) → B(a)(f ∼ g) ≡ (a : A) → (f(a) = g(a)).$

### Equivalence Relation

$reflexivity_∼ : (b : (a : A) → B(a)) → (b ∼ b). symmetry_∼ : (f, g : (a : A) → B(a)) → (f ∼ g) → (g ∼ f). transitivity_∼ : (f, g, h : (a : A) → B(a)) → (f ∼ g) → (g ∼ h) → (f ∼ h).$

#### Lemma

$(a : A) → f, g : B → H : f ∼ g, p : x =_A y → H(x) ⋅ g(p) = f(p) ⋅ H(y).$

#### Corollary

$(a : A) → f : A → H : f → id_A →(a : A) → H(f(x)) = f(H(x)).$

### Quasi-Inverse

Homotopy equivalence, 'equivalence of (higher) groupoids'.

$(f : A → B), qinv ≡ (g : B → A) × (f g ∼ id_B) × (g f ∼ id_A).$

#### Example

$(id_A, ↺_y, ↺_x) : qinv(id_A).$





### Equivalence

$1. (a : A) → f : B → qinv(f) → is-equiv(f). 2. (a : A) → f : B → is-equiv(f) → qinv(f). 3. e_1, e_2 : is-equiv(f) → e_1 = e_2. g ∼β h ◦ f ◦ g ∼α h, A ≃ B ≡ (f : A → B), is-equiv(f).$

#### Lemma

$1. A ≃ A. 2. A ≃ B → B ≃ A. 3. A ≃ B → B ≃ C → A ≃ C.$

## ×

### Theorem

$(x =A × B y) → (pr1(x) =A pr1(y)) × (pr3(x) =B pr3(y)).$







## Dependent ×

### Theorem

$w, w' : (a : A, P) →(w = w') ≃ p : w_0 = w'_0, p_*(w_1) = w'_1.$

### Propositional uniqueness principle

$z : (a : A) × P(a) → z = (pr1(z), pr3(z)).$

#### Theorem

$A : U, a : A → P : U, (a : A, p : P) → Q : U \under[→] a : A → (p : P, Q). p : x =_A y, (u, z) : (p : P, Q) \under[→] p_*(u, z) = (p_*(u), pair^=(p, ↺_[p_*(u)])_*(z)).$

## 𝟏

#### Theorem

$x, y : 𝟏 → (x = y) ≃ 𝟏.(x = y) → 𝟏, relf_⋆ : x = y, 𝟏 → (x = y),$

## Π-types and the function extensionality axiom

### Function extensionality

$a : A → B : U → f, g : B →(f = g) ≃ (a : A → f(a) =_[B(a)] g(a)). happly : (f =_B g) → (a : A → f(a) =_[B(a)] g(x)), _ : is-equiv(happly). funext : (a : A → f =_B g) → f =_B g.$

### Lemma

$x : X → A, B : U, p : x =_X y, (a : A → f : B), (a : A → g : B) →(p_*(f) = g) ≃ (a : A → p_*(f) = g(p_*)).$

### Lemma

$x : X, A : U, a : A, B : U, b : B, p : x =_X y,(x : X → a : A, f : B), (y : X → a : A, g : B) →(p_*(f) = g) ≃ (a : A →).$

## Universes and the univalence axiom

### Lemma

$A, B : U → idtoeqv : (A = B) → (A ≃ B).$

### Univalence

$(A = B) ≃ (A ≃ B).$

### Introduction rule for =𝒰

$ua : (A ≃ B) → (A = B).$

### Elimination rule for =𝒰

$idtoeqv ≡ transport^[X → X] : (A = B) → (A ≃ B).$

### Propositional computation rule for =𝒰

$transport^[X → X](ua(f), x) = f(x).$

### Propositional uniqueness rule for =𝒰

$p = ua(transport(p)).$
• ↺_A = ua(id_A).
• ua(f) ⋅ ua(g) = ua(g ◦ f).
• ua(f)^[−1] = ua(f^[−1]).

## =

### Theorem

$(a =_A a') → (b(a) =_B b(a'))$

## +

$(inj_1(a) = inj_1(a')) ≃ (a = a')(inj_2(b) = inj_2(b')) ≃ (b = b')(inj_1(a) = inj_2(b)) ≃ 𝟎 code(inj_1(a)) ≡ (a_0 = a), code(inj_2(b)) ≡ 𝟎.$

## ℕ

$code : ℕ → ℕ → U, code(0, 0) ≡ 𝟏, code(succ(m), 0) ≡ 𝟎, code(0, succ(n)) ≡ 𝟎, code(succ(m), succ(n)) ≡ code(m, n). r : n : N → code(n, n), r(0) ≡ ⋆, r(succ(n)) ≡ r(n).$

### Theorem

$m, n : ℕ → (m = n) ≃ code(m, n). encode : m, n : ℕ → (m = n) → code(m, n), encode(m, n, p) ≡ transport^[code(m, –)](p, r(m)), decode : m, n : ℕ → code(m, n) → (m = n) (by double induction on m, n). code(succ(m), succ(n)) ≡ code(m, n)→decode(m, n) (m = n)→ap_[succ] succ(m) = succ(n).$

## Equality of Structures

### Semigroup structures

$(m : A → A → A, x, y, z : A) → m(x, m(y, z)) = m(m(x, y), z)$

## Universal Properties

### ×

#### Mapping in, non-dependent.

$(C → A × B) ≃ (C → A) × (C → B).$$f : X → A × Bpr1 f : X → A pr3 f : X → B(pr1 f, pr3 f) : (X → A) × (X → B) ×-introductionλf.(pr1 f, pr3 f) : (X → A × B) → ((X → A) × (X → B)) →-introduction.$$a : X → A b : X → B(a, b) : (X → A) × (X → B) ×-introductionλ(a, b).λx.(a x, b x) : ((X → A) × (X → B)) → (X → A × B) →-introduction.$$ind(X → A) × (X → B)(C, c, (a, b)) ≡ c(a)(b),ind(X → A) × (X → B) : (C : ((X → A) × (X → B)) → 𝒰) → ((a : X → A) → (b : X → B) → C((a, b))) → (x : (X → A) × (X → B)) → C(x).λx.((pr1 f x, pr3 f x)) ≡ f,(λx.a(x), λx.b(x)) ≡ (a, b).$

#### Mapping in, dependent.

$((x : X) → (A(x) × B(x))) → ((x : X) → A(x)) × ((x : X) → B(x))$

Mapping out, non-dependent.

$((A × B) → C) ≃ (A → (B → C)).$

Mapping out, dependent.

$((w : A × B) → C(w)) ≃ ((a : A) → ((b : B) → C(a, b))).$

### Dependent ×

#### Mapping in, dependent.

Axiom of chice.

$(x : X) → ((a : A(x)) × B(x)(a)) ≃ (a : (x : X) → A(x)) × ((x : X) → B(x)(a(x))).$

#### Mapping out, dependent.

$((b : (a : A) × B(a)) → C(b)) ≃ ((a : A) → ((b : B(a)) → C(a, b))).$

### +

$(A + B → C) ≃ (A → C) × (B → C).$

### 𝟎

#### ?

$((x : A) → (p : a = x) B(x, p)) ≃ B(a, refl_a). f : A → C g : B → C A ×_C B ≡ (a : A) × (b : B) (f(a) = g(b)).$

## 𝕊1

'Circle'.

### Formation Rule

$𝕊1 : 𝒰.$



## 𝕀

'Interval'.

### Formation Rule

$𝕀 : 𝒰.$

### Function Extensionality

#### Lemma

$is-truncated_[−2](𝕀).$

#### Lemma

$(f, g : A → B) → (a : A → f(a) = g(a)) → (f =_[A → B] g).$

### Circle and Sphere

loop ≠ ↺_[base].

#### Lemma

$f : (x : 𝕊^1) → (x = x), f ≠ x ↦ ↺_x.$

#### Corollary

$𝕊^1 : U, is-truncated_1(U) → 0.$

#### Lemma

$f : A → B, x, y : A, p, q : x = y, r : p = q → ap_f^2(↺_p) ≡ ↺_[f(p)].$

#### Lemma

$P : A → U, x, y : A, p, q : x = y, r : p = q, u : P(x) → transport^2(r, u) : p_*(u) = q_*(u).$

### Suspension

• N : ΣA,
• S : ΣA,
• merid : A → (N =_[ΣA] S).

#### Lemma

$Σ𝟐 ≃ S_1.$

#### Lemma

$A, (B, b_0) : U → Map_*(A_+, B) ≃ (A → B).$

#### Lemma

$(A, a_0), (B, b_0) : U → Map_*(ΣA, B) ≃ Map_*(A, ΩB).$

### Truncation

#### Lemma

$(||A ∪^C B||_0 → E)≃coconeD(E).$

### Algebra

#### Theorem

$(F(A) →_[Group] G) ≃ (A → G).$

### Monoid

$is-0-type(G) →$
• (x, y) ↦ x y : G × G → G,
• 1 : G,
• (x : G) → (x 1 = x) × (1 x = x),
• (x, y, z : G) → x (y z) = (x y) z.

### Group

• x ↦ x^[−1] : G → G,
• (x : G) → (x x^[−1] = 1) × (x^[−1] x = 1).

### General Syntax

#### Example

$f : (X : 𝒰) → X → X, f_X ≡ id_X, f_2 : 2 → 2. a, b : K, σ : f_K(a) → f_K(b).$

### Quotient

$(a, b : A) × R(a, b) ⇉ A.$
• q : A → A / R,
• (a, b : A) → R(a, b)(q(a) = q(b)),
• (x, y : A / R) → (r, s : x = y) → (r = s).

### Integers

$(a, b) ∼ (c, d) ≡ (a + d = b + c) → Z ≡ (N × N) / ∼.$

#### Lemma

$idempotent r : A → A, x, y : A → (r(x) = r(y)) ≃ (x ∼ y) →(A / ∼) ≡ ((x : A) × r(x) = x), q : A → (A / ∼),((A / ∼) → B) ≃ ((g : A → B) × x, y : A → (x ∼ y) → (g(x) = g(y))).$

#### Lemma

$P : Z → U,$
• d_0 : P(0),
• d_+ : (n : N) → P(n) → P(succ(n)),
• d_− : (n : N) → P(−n) → P(−succ(n))

→ f : z : Z → P(z),

• f(0) = d_0,
• (n : N) → f(succ(n)) = d_+(n, f(n)),
• (n : N) → f(−succ(n)) = d_−(n, f(−n)).

#### Corollary

$p : a = a, n ↦ p_n : (n : Z) → (a = a), p^0 ≡ ↺_a, p^[n + 1] ≡ p^n p for 0 ≤ n, p^[n − 1] ≡ p^n p^[−1] for n ≤ 0.$