Homotopy Type Theory Contents 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 Homotopies and Equivalences Homotopies Equivalence Relation Quasi-Inverse Equivalence 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 𝟏 Π-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 × Dependent × + 𝟏 𝟎 Higher Inductive Types 𝕊1 Formation Rule Introduction Rules Induction principle and dependent path 𝕀 Formation Rule Introduction Rules Recursion Principle Function Extensionality Circle and Sphere Suspension Cell Complex Hub and Spoke Pushout Truncation Quotient Algebra Monoid Group Flattening Lemma General Syntax Quotient Integers Homotopy Type Modal Homotopy Type Theory Cohesive Homotopy Type Theory References 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 = 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 : 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) , refl a ) ) : ( 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. × Theorem ( x = A × B y) → ( pr 1 ( x) = A pr 1 ( y) ) × ( 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 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 = ( pr 1 ( z) , pr 3 ( 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) .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 × B pr 1 f : X → A pr 3 f : X → B( pr 1 f, pr 3 f) : ( X → A) × ( X → B) ×-introductionλf.( pr 1 f, pr 3 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.( ( pr 1 f x, pr 3 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'.
𝕊 1 : 𝒰 .Introduction Rules base : 𝕊 1 , loop : base = 𝕊 1 base Induction principle and dependent path 𝕀 'Interval'.
𝕀 : 𝒰 .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) ≃ cocone D ( 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 Modal Homotopy Type Theory Cohesive Homotopy Type Theory References