Homotopy Type Theory

Homotopy

f, g : X \to Y, H : X \times [0, 1] \to Y \to 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 =_{A} y} q .

Types Are Higher Groupoids

inverse : =-symmetry

First proof.

λ (A) . λ (a) . λ (b) . λ (p) . {ind}_{=_{A}} (λ (a) . λ (b) . λ (p) . (a = b), λ (a) . {refl}_{a}, a, b, p) : (A : 𝒰) \to (a, b : A) \to (a = b) \to (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), {refl}_{a})) : (A : 𝒰) \to (a, b, c : A) \to (a = b) \to (b = c) \to (a = c) .

Lemma

\frac{A : 𝒰 x, y, z, w : A p : x = y, q : y = z, r : z = w}{1 . p = p \cdot ↺_{y}, p = ↺_{x} \cdot p . 2 . p^{- 1} \cdot p = ↺_{y}, p \cdot p^{- 1} = ↺_{x} . 3 . (p^{- 1})^[−1] = p . 4 . p \cdot (q \cdot r) = (p \cdot q) \cdot r .}

Eckmann–Hilton

α, β : Ω^{2} (A, a) \to α \cdot β = β \cdot α .

Pointed type

(A, a) : 𝒰_{•} \equiv (A : 𝒰, A) .

Loop space

Ω (A, a) \equiv (a =_{A} a, ↺_{a}) .

Ω^{0} (A, a) \equiv (A, a)

Ω^{n + 1} (A, a) \equiv Ω^{n} (Ω (A, a)) .

Ω^{2} (A, a) \equiv Ω (Ω (A, a)) \equiv Ω ((a =_{A} a, ↺_{a})) . \equiv Ω (a =_{A} a, ↺_{a}) \equiv (↺_{a} =_{a =_{A} a} ↺_{a}, ↺_{↺_{a}}) .

Functions Are Functors

Lemma

f : A \to B, x, y : A, {ap}_{f} : (x =_{A} y) \to (f (x) =_{B} f (y)) .

D \equiv (x, y, p) \mapsto f (x) = f (y), D : x, y : A \to (x = y) \to 𝒰, d \equiv x \mapsto ↺_{f (x)}, d : x : A \to D (x, x, ↺_{x}), {ap}_{f} : x, y : A \to (x = y) \to (f (x) = f (y)) (by path induction) . x : A \to ap_f (↺_{x}) \equiv ↺_[f (x)] (by computation rule) .

Lemma

Dependent Types are Fibrations

Transport

a : A \to P : 𝒰 \to p : x =_{A} y \to p_{*} \equiv {transport}^{P} (p, -) \equiv {ind}_{=_{A}} (D, d, x, y, p) : P (x) \to P (y), D \equiv x, y : A, p : x =_{A} y \to P (x) = P (y), d \equiv x : A \to {id}_{P (x)}, {ind}_{=_{A}} (D, d, x, y, p) : P (x) \to 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 : 𝒰 \to a : A \to P : 𝒰, a_0 : A, p_0 : P \to p : x =_{A} y \to lift (p_{0}, p) : (x, p_{0}) = (y, p_{*} (p_{0})), {pr}_{1} (lift (p_{0}, p)) = p .

Dependent map

a : A \to p : P \to p : x =_{A} y \to p_{*} (f (x)) =_{P (y)} f (y) . D \equiv x, y, p \to, (↺_{x})_* (f (x)) \equiv f (x), d \equiv x : A \to ↺_{f (x)},

Lemma

(f (x) = f (y)) \to (p_{*} (f (x)) = f (y)), (p_{*} (f (x)) = f (y)) \to (f (x) = f (y)) .

Lemma

a : A \to P : U, p : x =_{A} y, q : y =_{A} z, p_0 : P (x) \to q_* (p_{*} (p_0)) = (p q)_* (p_0) .

Lemma

a : A \to b : B, b : B \to P : U, p : x =_{A} y, p_0 : P (b (x)) \to

Lemma

a : A \to P, Q : U, (a : A \to P \to Q), p : x =_{A} y, p_0 : P (b (x)) \to

Homotopies and Equivalences

Homotopies

Natural transformations.

\frac{f, g : (a : A) \to B (a)}{(f \sim g) \equiv (a : A) \to (f (a) = g (a))} .

Equivalence Relation

\begin{array}{l} {reflexivity}_{\sim} : (f : (a : A) \to B (a)) \to (f \sim f) . \\ {symmetry}_{\sim} : (f, g : (a : A) \to B (a)) \to (f \sim g) \to (g \sim f) . \\ {transitivity}_{\sim} : (f, g, h : (a : A) \to B (a)) \to (f \sim g) \to (g \sim h) \to (f \sim h) . \end{array}

Lemma

(a : A) \to f, g : B \to H : f \sim g, p : x =_{A} y \to H (x) \cdot g (p) = f (p) \cdot H (y) .

Corollary

(a : A) \to f : A \to H : f \to {id}_{A} \to (a : A) \to H (f (x)) = f (H (x)) .

Quasi-Inverse

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

(f : A \to B), qinv \equiv (g : B \to A) \times (f g \sim {id}_{B}) \times (g f \sim {id}_{A}) .

Example

({id}_{A}, ↺_{y}, ↺_{x}) : qinv ({id}_{A}) .

Example

Equivalence

$(a : A) \to f : B \to qinv (f) \to is-equiv (f) .$
$(a : A) \to f : B \to is-equiv (f) \to qinv (f) .$
$e_{1}, e_{2} : is-equiv (f) \to e_{1} = e_{2}$ .

g \overset{β}{\sim} h ◦ f ◦ g \overset{α}{\sim} h, A ≃ B \equiv (f : A \to B), is-equiv (f) .

Lemma

$A ≃ A .$
$A ≃ B \to B ≃ A .$
$A ≃ B \to B ≃ C \to A ≃ C .$

The Higher Groupoid Structure of Type Formers

×

Theorem

(x =_{A \times B} y) \to ({pr}_{1} (x) =_{A} {pr}_{1} (y)) \times ({pr}_{3} (x) =_{B} {pr}_{3} (y)) .

Introduction Rule for =_A×B

Elimination Rule for =_A×B

Propositional Computation Rule for =_A×B

Propositional Uniqueness Principle for =_A×B

Theorem

Dependent ×

Theorem

w, w' : (a : A, P) \to (w = w') ≃ p : w_{0} = {w'}_{0}, p_{*} (w_{1}) = {w'}_{1} .

Propositional Uniqueness Principle

z : (a : A) \times P (a) \to z = ({pr}_{1} (z), {pr}_{3} (z)) .

Theorem

A : 𝒰, a : A \to P : 𝒰, (a : A, p : P) \to Q : 𝒰 \underset{\to}{0} a : A \to (p : P, Q) .

p : x =_{A} u, (u, z) : (p : P, Q) \underset{\to}{0} p_{*} (u, z) = (p_{*} (u), {pair}^{= {(p, ↺_{p_{*} (u)})}_{*}} (z)) .

𝟏

Theorem

x, u : 𝟏 \to (x = u) ≃ 𝟏 .

(x = u) \to 𝟏, {relf}_{⋆} : x = u, 𝟏 \to (x = u),

Π-Types and the Function Extensionality Axiom

Function Extensionality

a : A \to B : 𝒰 \to f, g : B \to (f = g) ≃ (a : A \to f (a) =_{B (a)} g (a)) .

happly : (f =_{B} g) \to (a : A \to f (a) =_{B (a)} g (x)),_: is-equiv (happly) .

funext : (a : A \to f =_{B} g) \to f =_{B} g .

Lemma

x : X \to A, B : 𝒰, p : x =_{X} y, (a : A \to f : B), (a : A \to g : B) \to (p_{*} (f) = g) ≃ (a : A \to p_{*} (f) = g (p_{*})) .

Lemma

x : X, A : 𝒰, a : A, B : 𝒰, b : B, p : x =_{X} y, (x : X \to a : A, f : B), (y : X \to a : A, g : B) \to (p_{*} (f) = g) ≃ (a : A \to) .

Universes and the Univalence Axiom

Lemma

A, B : 𝒰 \to idtoeqv : (A = B) \to (A ≃ B) .

Univalence

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

Remark

Introduction rule for =_𝒰

ua : (A ≃ B) \to (A = B) .

Elimination Rule for =_𝒰

idtoeqv \equiv {transport}^{X \to X} : (A = B) \to (A ≃ B) .

Propositional Computation Rule for =_𝒰

{transport}^{X \to X} (ua (f), x) = f (x) .

Propositional Uniqueness Rule for =_𝒰

p = ua (transport (p)) .

$↺_{A} = ua ({id}_{A})$ .
$ua (f) \cdot ua (g) = ua (g ◦ f)$ .
${ua (f)}^{- 1} = ua (f^{- 1})$ .

Lemma

=

Theorem

(a =_{A} a') \to (b (a) =_{B} b (a'))

Lemma

Theorem

+

({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)) \equiv (a_{0} = a), code ({inj}_{2} (b)) \equiv 𝟎 .

Theorem

ℕ

code : ℕ \to ℕ \to 𝒰,

code (0, 0) \equiv 𝟏,

code (succ (m), 0) \equiv 𝟎,

code (0, succ (n)) \equiv 𝟎,

code (succ (m), succ (n)) \equiv code (m, n) .

r : n : ℕ \to code (n, n), r (0) \equiv ⋆, r (succ (n)) \equiv r (n) .

Theorem

(m, n : ℕ) \to (m = n) ≃ code (m, n) .

encode : (m, n) : ℕ \to (m = n) \to code (m, n),

encode (m, n, p) \equiv {transport}^{code (m, -)} (p, r (m)),

decode : m, n : ℕ \to code (m, n) \to (m = n) (by double induction on m, n) .

code (succ (m), succ (n)) \equiv code (m, n) \overset{decode (m, n)}{\to} (m = n) \overset{{ap}_{succ}}{\to} succ (m) = succ (n) .

Equality of Structures

Semigroup structures

(m : A \to A \to A, x, y, z : A) \to m (x, m (y, z)) = m (m (x, y), z)

Universal Properties

×

Mapping in, non-dependent.

(C \to A \times B) ≃ (C \to A) \times (C \to B) .

\frac{\frac{\frac{f : X \to A \times B}{{pr}_{1} f : X \to A {pr}_{3} f : X \to B}}{({pr}_{1} f, {pr}_{3} f) : (X \to A) \times (X \to B)} ×-introduction}{λ f . ({pr}_{1} f, {pr}_{3} f) : (X \to A \times B) \to ((X \to A) \times (X \to B))} →-introduction .

\frac{\frac{a : X \to A, b : X \to B}{(a, b) : (X \to A) \times (X \to B)} ×-introduction}{λ (a, b) . λ x . (a x, b x) : ((X \to A) \times (X \to B)) \to (X \to A \times B)} →-introduction .

By induction principle for ×.

\begin{array}{l} {ind}_{(X \to A) \times (X \to B)} (C, c, (a, b)) \equiv c (a) (b), \\ {ind}_{(X \to A) \times (X \to B)} : (C : ((X \to A) \times (X \to B)) \to 𝒰) \to ((a : X \to A) \to (b : X \to B) \to C ((a, b))) \to (x : (X \to A) \times (X \to B)) \to C (x) . \\ λ x . (({pr}_{1} f x, {pr}_{3} f x)) \equiv f, \\ (λ x . a (x), λ x . b (x)) \equiv (a, b) . \end{array}

Mapping in, dependent.

((x : X) \to (A (x) \times B (x))) \to ((x : X) \to A (x)) \times ((x : X) \to B (x))

Mapping out, non-dependent.

((A \times B) \to C) ≃ (A \to (B \to C)) .

Mapping out, dependent.

((w : A \times B) \to C (w)) ≃ ((a : A) \to ((b : B) \to C (a, b))) .

Dependent ×

Mapping in, dependent.

Axiom of choice.

(x : X) \to ((a : A (x)) \times B (x) (a)) ≃ (a : (x : X) \to A (x)) \times ((x : X) \to B (x) (a (x))) .

Mapping out, dependent.

((b : (a : A) \times B (a)) \to C (b)) ≃ ((a : A) \to ((b : B (a)) \to C (a, b))) .

+

(A + B \to C) ≃ (A \to C) \times (B \to C) .

𝟏

𝟎

?

((x : A) \to (p : a = x) B (x, p)) ≃ B (a, {refl}_{a}) . f : A \to C g : B \to C A \times_{C} B \equiv (a : A) \times (b : B) (f (a) = g (b)) .

Higher Inductive Types

𝕊¹

'Circle'.

Formation Rule

\frac{}{𝕊^{1} : 𝒰} .

Introduction Rules

\frac{}{base : 𝕊^{1}}, \frac{}{loop : base =_{𝕊^{1}} base}

Induction principle and dependent path

𝕀

'Interval'.

Formation Rule

\frac{}{𝕀 : 𝒰} .

Introduction Rules

\frac{}{0_{𝕀} : 𝕀}, \frac{}{1_{𝕀} : 𝕀}, \frac{}{seg : 0_{𝕀} =_{𝕀} 1_{𝕀}}

Recursion Principle

Function Extensionality

Lemma

{is-truncated}_{- 2} (𝕀) .

Lemma

(f, g : A \to B) \to (a : A \to f (a) = g (a)) \to (f =_{A \to B} g) .

Circle and Sphere

Lemma

loop \neq ↺_{base} .

Lemma

f : (x : 𝕊^{1}) \to (x = x), f \neq x \mapsto ↺_{x} .

Corollary

𝕊^{1} : 𝒰, is-truncated_1 (𝒰) \to 𝟎 .

Lemma

f : A \to B, x, y : A, p, q : x = y, r : p = q \to {ap}_{f^{2}} (↺_{p}) \equiv ↺_{f (p)} .

Lemma

P : A \to 𝒰, x, y : A, p, q : x = y, r : p = q, u : P (x) \to {transport}^{2} (r, u) : p_{*} (u) = q^{*} (u) .

Lemma

Suspension

$N : ΣA$ ,
$S : ΣA$ ,
$merid : A \to (N =_{ΣA} S)$ .

Lemma

Σ𝟐 ≃ S_1 .

Lemma

A, (B, b_{0}) : U \to {Map}_{*} (A_{+}, B) ≃ (A \to B) .

Lemma

(A, a_{0}), (B, b_{0}) : 𝒰 \to {Map}_{*} (ΣA, B) ≃ {Map}_{*} (A, ΩB) .

Cell Complex

Hub and Spoke

Pushout

Truncation

Lemma

({|| A ∪^C B ||}_{0} \to E) ≃ {cocone}_{D} (E) .

Quotient

Algebra

Theorem

(F (A) \to_{Group} G) ≃ (A \to G) .

Monoid

is-0-type (G) \to

$(x, y) \mapsto x y : G \times G \to G$ ,
$1 : G$ ,
$(x : G) \to (x 1 = x) \times (1 x = x)$ ,
$(x, y, z : G) \to x (y z) = (x y) z$ .

Group

$x \mapsto x^{- 1} : G \to G$ ,
$(x : G) \to (x x^{- 1} = 1) \times (x^{- 1} x = 1)$ .

Flattening Lemma

General Syntax

Example

f : (X : 𝒰) \to X \to X, f_{X} \equiv {id}_{X}, f_{2} : 2 \to 2 . a, b : K, σ : f_{K} (a) \to f_{K} (b) .

Quotient

(a, b : A) \times R (a, b) ⇉ A .

$q : A \to A / R$ ,
$(a, b : A) \to R (a, b) \to (q (a) = q (b))$ ,
$(x, y : A / R) \to (r, s : x = y) \to (r = s)$ .

Integers

(a, b) \sim (c, d) \equiv (a + d = b + c) \to Z \equiv (N \times N) / \sim .

Lemma

idempotent r : A \to A, x, y : A \to (r (x) = r (y)) ≃ (x \sim y) \to (A / \sim) \equiv ((x : A) \times r (x) = x), q : A \to (A / \sim), ((A / \sim) \to B) ≃ ((g : A \to B) \times x, y : A \to (x \sim y) \to (g (x) = g (y))) .

Corollary

Lemma

P : Z \to U,

$d^{0} : P (0)$ ,
$d_+ : (n : ℕ) \to P (n) \to P (succ (n))$ ,
$d_− : (n : ℕ) \to P (- n) \to P (- succ (n))$

\to f : z : Z \to P (z),

$f (0) = d_{0}$ ,
$(n : ℕ) \to f (succ (n)) = d_+ (n, f (n)),$
$(n : ℕ) \to f (- succ (n)) = d_− (n, f (- n)) .$

Corollary

p : a = a, n \mapsto p_{n} : (n : ℤ) \to (a = a), p^{0} \equiv ↺_{a}, p^{n + 1} \equiv p^{n} p for 0 \leq n, p^{n - 1} \equiv p^{n} p^{- 1} for n \leq 0 .

Homotopy Type Theory

Homotopy

Types Are Higher Groupoids

inverse : =-symmetry

concatenate/compose : =-transitivity

Lemma

Eckmann–Hilton

Pointed type

Loop space

Functions Are Functors

Lemma

Lemma

Dependent Types are Fibrations

Transport

Transport

Path Lifting Property

Dependent map

Lemma

Lemma

Lemma

Lemma

Lemma

Homotopies and Equivalences

Homotopies

Equivalence Relation

Lemma

Corollary

Quasi-Inverse

Example

Example

Example

Equivalence

Lemma

The Higher Groupoid Structure of Type Formers

×

Theorem

Introduction Rule for =A×B

Elimination Rule for =A×B

Propositional Computation Rule for =A×B

Propositional Uniqueness Principle for =A×B

Theorem

Theorem

Dependent ×

Theorem

Propositional Uniqueness Principle

Theorem

𝟏

Theorem

Π-Types and the Function Extensionality Axiom

Function Extensionality

Lemma

Lemma

Universes and the Univalence Axiom

Lemma

Univalence

Remark

Introduction rule for =𝒰

Elimination Rule for =𝒰

Propositional Computation Rule for =𝒰

Propositional Uniqueness Rule for =𝒰

Lemma

=

Theorem

Lemma

Lemma

Theorem

Theorem

+

Theorem

ℕ

Theorem

Equality of Structures

Semigroup structures

Universal Properties

×

Mapping in, non-dependent.

Mapping in, dependent.

Dependent ×

Mapping in, dependent.

Mapping out, dependent.

Introduction Rule for =_A×B

Elimination Rule for =_A×B

Propositional Computation Rule for =_A×B

Propositional Uniqueness Principle for =_A×B

Introduction rule for =_𝒰

Elimination Rule for =_𝒰

Propositional Computation Rule for =_𝒰

Propositional Uniqueness Rule for =_𝒰

𝕊¹