Homotopy Type Theory

Wikipedia nLab

Contents

Homotopy

Wikipedia nLabf, 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).

Lemma

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

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).

Example

Example

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.

The Higher Groupoid Structure of type formers

×

Theorem

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

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

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[0][→] a : A → (p : P, Q). p : x =_A y, (u, z) : (p : P, Q) \under[0][→] 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).

Remark

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]).

Lemma

=

Theorem

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

Lemma

Lemma

Theorem

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))(a_0 = a), code(inj_2(b)) ≡ 𝟎.

Theorem

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.

By type theory#×-induction.

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)).

Higher Inductive Types

𝕊1

'Circle'.

Formation Rule

𝕊1 : 𝒰.

Introduction Rules

base : 𝕊1,  loop : base =𝕊1 base

Induction principle and dependent path

𝕀

'Interval'.

Formation Rule

𝕀 : 𝒰.

Introduction Rules

0𝕀 : 𝕀,  1𝕀 : 𝕀,  seg : 0𝕀 =𝕀 1𝕀

Recursion Principle

Function Extensionality

Lemma

is-truncated_[−2](𝕀).

Lemma

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

Circle and Sphere

Lemma

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).

Lemma

Suspension

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

Lemma

Σ𝟐 ≃ S_1.

Lemma

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).

Cell Complex

Hub and Spoke

Pushout

Truncation

Lemma

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

Quotient

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).

Flattening Lemma

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))).

Corollary

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.

Homotopy Type

Cohesive Homotopy Type Theory

References