module HoTT where
The HoTT Book?🔗
While the 1Lab has not been consciously designed as a project to formalise the HoTT book, in the course of our explorations into formalised univalent mathematics, we have formalised a considerable subset of the first part, and most of chapter 9. The vast majority of the 1Lab is material that was not covered in the HoTT book.
Part 1 Foundations🔗
Chapter 2 Homotopy type theory🔗
2.1 Types are higher groupoids🔗
_ = sym _ = _∙_ _ = ∙-id-l _ = ∙-id-r _ = ∙-inv-l _ = ∙-inv-r _ = ∙-assoc _ = Ωⁿ⁺²-is-abelian-group _ = Type∙ _ = Ωⁿ
- Lemma 2.1.1: sym
- Lemma 2.1.2: _∙_
- Lemma 2.1.4:
- Theorem 2.1.6: Ωⁿ⁺²-is-abelian-group
- Definition 2.1.7: Type∙
- Definition 2.1.8: Ωⁿ
2.2 Functions are functors🔗
- Lemma 2.2.1: ap
- Lemma 2.2.2:
- ap-comp-path
- Definitional in cubical type theory
- Definitional in cubical type theory
- Definitional in cubical type theory
2.3 Type families are fibrations🔗
- Lemma 2.3.1: subst
- Lemma 2.3.2: Σ-pathp
- Lemma 2.3.4: Our ap is dependent by nature.
- Lemma 2.3.5: transport-refl
- Lemma 2.3.9: subst-∙
- Lemma 2.3.10: Definitional in cubical type theory
2.4 Homotopies and equivalences🔗
_ = homotopy-natural _ = homotopy-invert _ = is-iso _ = transport⁻transport _ = id-equiv _ = Equiv.inverse _ = _∙e_
- Lemma 2.4.3: homotopy-natural
- Lemma 2.4.4: homotopy-invert
- Lemma 2.4.6: is-iso
- Example 2.4.9: transport⁻transport
- Lemma 2.4.12: id-equiv, Equiv.inverse,
_∙e_
2.7 Cartesian product types🔗
- Theorem 2.7.2: Σ-pathp-iso
- Theorem 2.7.3: Agda has definitional η equality for records.
2.9 Π-types and function extensionality🔗
- Theorem 2.9.3: funext (no longer an axiom)
- Lemma 2.9.6: funext-dep (no longer an axiom)
2.10 Universes and univalence🔗
- Lemma 2.10.1: path→equiv
- Theorem 2.10.3: univalence
- ua, uaβ
- ua-id-equiv, ua∙, sym-ua
2.11 Identity type🔗
_ = is-equiv→is-embedding _ = subst-path-left _ = subst-path-right _ = transport-path _ = commutes→square
- Theorem 2.11.1: is-equiv→is-embedding
- Lemma 2.11.2: subst-path-left, subst-path-right, transport-path
- Theorem 2.11.5: commutes→square
2.12 Coproducts🔗
- Theorem 2.12.5: ⊎Path.Code≃Path
Chapter 3 Sets and Logic🔗
3.1 Sets and n-types🔗
- Definition 3.1.1: is-set
- Example 3.1.2: Definitional in cubical type theory.
- Example 3.1.4: Nat-is-set
- Example 3.1.5: ×-is-hlevel (special case)
- Example 3.1.6: Π-is-hlevel (special case)
- Definition 3.1.7: is-groupoid
- Lemma 3.1.8: is-hlevel-suc (special case)
3.3 Mere propositions🔗
- Definition 3.3.1: is-prop
- Lemma 3.3.3: prop-ext
- Lemma 3.3.4: is-prop→is-set
- Lemma 3.3.5: is-prop-is-prop, is-hlevel-is-prop
3.5 Subsets and propositional resizing🔗
- Lemma 3.5.1: Σ-prop-path
- Axiom 3.5.5: Ω, □.
3.7 Propositional truncation🔗
The type itself is defined as a higher-inductive type ∥_∥. We also define ∃ as a shorthand for the truncation of Σ
.
3.9 The principle of unique choice🔗
- Lemma 3.9.1: is-prop→equiv∥-∥
- Lemma 3.9.2: Implicit in e.g.
∥-∥-univ
, ∥-∥-proj
3.11 Contractibility🔗
- Definition 3.11.1: is-contr
- Definition 3.11.4: is-contr-is-prop
- Definition 3.11.7: retract→is-contr
- Definition 3.11.8: Singleton-is-contr
Exercises🔗
_ = equiv→is-hlevel _ = ⊎-is-hlevel _ = Σ-is-hlevel _ = contractible-if-inhabited _ = H-Level-Dec _ = disjoint-⊎-is-prop _ = ℕ-well-ordered _ = is-prop≃equiv∥-∥ _ = Finite-choice
- Exercise 3.1: equiv→is-hlevel
- Exercise 3.2: ⊎-is-hlevel
- Exercise 3.3: Σ-is-hlevel
- Exercise 3.5: contractible-if-inhabited
- Exercise 3.6: H-Level-Dec
- Exercise 3.7: disjoint-⊎-is-prop
- Exercise 3.19: ℕ-well-ordered
- Exercise 3.21: is-prop≃equiv∥-∥
- Exercise 3.22: Finite-choice
Chapter 4 Equivalences🔗
4.2 Half adjoint equivalences🔗
_ = is-half-adjoint-equiv _ = is-iso→is-half-adjoint-equiv _ = fibre _ = fibre-paths _ = is-half-adjoint-equiv→is-equiv _ = linv _ = rinv _ = is-equiv→pre-is-equiv _ = is-equiv→post-is-equiv _ = is-iso→is-contr-linv _ = is-iso→is-contr-rinv
- Definition 4.2.1: is-half-adjoint-equiv
- Definition 4.2.3: is-iso→is-half-adjoint-equiv
- Definition 4.2.4:
fibre
- Lemma 4.2.5:
fibre-paths
- Theorem 4.2.6: is-half-adjoint-equiv→is-equiv
- Definition 4.2.7: linv, rinv
- Lemma 4.2.8: is-equiv→pre-is-equiv, is-equiv→post-is-equiv
- Lemma 4.2.9: is-iso→is-contr-linv, is-iso→is-contr-rinv
4.3 Bi-invertible maps🔗
- Definition 4.3.1: is-biinv
- Theorem 4.3.2: is-biinv-is-prop
4.4 Contractible fibres🔗
Note: This is our “default” definition of equivalence, but we generally use it through the interface of half-adjoint equivalences.
- Definition 4.4.1: is-equiv
- Theorem 4.4.3: is-equiv→is-half-adjoint-equiv
- Lemma 4.4.4: is-equiv-is-prop
4.8 The object classifier🔗
- Lemma 4.8.1: Fibre-equiv
- Lemma 4.8.2: Total-equiv
- Theorem 4.8.3: Map-classifier
Chapter 6 Higher inductive types🔗
6.2 Induction principles and dependent paths🔗
- Remark 6.2.3: to-pathp, from-pathp
- _Induction principle for : by pattern matching.
- Lemma 6.2.5: S¹-rec
- Lemma 6.2.9: Ωⁿ≃Sⁿ-map for
n = 1
6.3 The interval🔗
This is the higher inductive type [0,1], not the interval type I.
- Lemma 6.3.1: interval-contractible
6.4 Circles and spheres🔗
- Lemma 6.4.1: refl≠loop
6.6 Cell complexes🔗
- The torus: T².
6.9 Truncations🔗
- Lemma 6.9.1: ∥-∥₀-elim
6.10 Quotients🔗
We define the quotient _/_ in terms of coequalisers Coeq.
- Lemma 6.10.3: Coeq-univ.
6.11 Algebra🔗
- Definition 6.11.1: Monoid-on, Group-on
- Definition 6.11.4: πₙ₊₁
- Lemma 6.11.5: Monoid.Free⊣Forget
- Lemma 6.11.6: Group.make-free-group
Chapter 7 Homotopy n-types🔗
7.1 Definition of n-types🔗
- Definition 7.1.1: is-hlevel
- Theorem 7.1.4: retract→is-hlevel
- Corollary 7.1.5: equiv→is-hlevel
- Theorem 7.1.7: is-hlevel-suc
- Theorem 7.1.8: Σ-is-hlevel
- Theorem 7.1.9: Π-is-hlevel
- Theorem 7.1.10: is-hlevel-is-prop
- Theorem 7.1.11: n-Type-is-hlevel
7.2 Uniqueness of identity proofs and Hedberg’s theorem🔗
_ = set-identity-system _ = identity-system→hlevel _ = Discrete→is-set _ = Discrete-Nat _ = hubs-and-spokes→hlevel _ = hlevel→hubs-and-spokes
- Theorem 7.2.2: set-identity-system, identity-system→hlevel
- Theorem 7.2.5: Discrete→is-set
- Theorem 7.2.6: Discrete-Nat
- Theorem 7.2.7: hubs-and-spokes→hlevel, hlevel→hubs-and-spokes
7.3 Truncations🔗
- Lemma 7.3.1: n-Tr-is-hlevel
- Lemma 7.3.2: n-Tr-elim
- Theorem 7.3.12:
n-Tr-path-equiv
Part 2 Mathematics🔗
Chapter 8 Homotopy theory🔗
The only non-trivial result worth mentioning from Chapter 8 is the fundamental group of the circle.
8.1 π₁(S¹)🔗
_ = S¹Path.Cover _ = S¹Path.encode _ = S¹Path.decode _ = S¹Path.encode-decode _ = S¹Path.encode-loopⁿ _ = ΩS¹≃integers
- Definition 8.1.1: S¹Path.Cover
- Definition 8.1.5: S¹Path.encode
- Definition 8.1.6: S¹Path.decode
- Lemma 8.1.7: S¹Path.encode-decode
- Lemma 8.1.8: S¹Path.encode-loopⁿ
- Corollary 8.1.10: ΩS¹≃integers
Chapter 9 Category theory🔗
Since a vast majority of the 1Lab’s mathematics consists of pure category theory, or mathematics done with a very categorical inclination, this is our most complete chapter.
9.1 Categories and Precategories🔗
_ = Precategory _ = is-invertible _ = _≅_ _ = is-invertible-is-prop _ = Cat[_,_] _ = ≅-is-set _ = path→iso _ = is-category _ = equiv-path→identity-system _ = Univalent.Ob-is-groupoid _ = Hom-transport _ = path→to-sym _ = path→to-∙ _ = Poset _ = Rel _ = Sets-is-category
- Definition 9.1.1: Precategory
- Definition 9.1.2: is-invertible, _≅_
- Lemma 9.1.3: is-invertible-is-prop, ≅-is-set
- Lemma 9.1.4: path→iso
- Definition 9.1.61: is-category
- Example 9.1.7: Sets-is-category
- Lemma 9.1.8: Univalent.Ob-is-groupoid
- Lemma 9.1.9: Hom-transport (9.1.10), path→to-sym (9.1.11), path→to-∙ (9.1.12/9.1.13)
- Example 9.1.14: Poset
- Example 9.1.19: Rel
9.2 Functors and Transformations🔗
_ = Functor _ = _=>_ _ = Nat-path _ = Nat-is-set _ = Functor-path _ = componentwise-invertible→invertible _ = Nat-iso→Iso _ = Functor-is-category _ = _F∘_ _ = _◂_ _ = _▸_ _ = F∘-assoc _ = Prebicategory.pentagon _ = Prebicategory.triangle _ = Cat
- Definition 9.2.1: Functor
- Definition 9.2.2: _=>_
- The paragraph immediately after 9.2.2 is Nat-path and Nat-is-set
- The one after that is Functor-path.
- Definition 9.2.3: Cat[_,_]
- Lemma 9.2.4: If: componentwise-invertible→invertible; Only if: Nat-iso→Iso
- Theorem 9.2.5: Functor-is-category
- Theorem 9.2.6: _F∘_
- Definition 9.2.7: _◂_, _▸_
- Lemma 9.2.9: F∘-assoc
- Lemma 9.2.10: See the definition of Prebicategory.pentagon for Cat.
- Lemma 9.2.11: See the definition of Prebicategory.triangle for Cat.
9.3 Adjunctions🔗
- Lemma 9.3.1: _⊣_
- Lemma 9.3.2: is-left-adjoint-is-prop
9.4 Equivalences🔗
_ = is-equivalence _ = is-faithful _ = is-full _ = is-fully-faithful _ = is-split-eso _ = is-eso _ = ff+split-eso→is-equivalence _ = Essential-fibre-between-cats-is-prop _ = ff+eso→is-equivalence _ = is-precat-iso _ = is-equivalence→is-precat-iso _ = is-precat-iso→is-equivalence _ = Precategory-identity-system _ = Category-identity-system
- Definition 9.4.1: is-equivalence
- Definition 9.4.3: is-faithful, is-full, is-fully-faithful
- Definition 9.4.4: is-split-eso
- Lemma 9.4.5: ff+split-eso→is-equivalence
- Definition 9.4.6: is-eso
- Lemma 9.4.7: Essential-fibre-between-cats-is-prop, ff+eso→is-equivalence
- Definition 9.4.8: is-precat-iso
- Lemma 9.4.14: is-equivalence→is-precat-iso, is-precat-iso→is-equivalence
- Lemma 9.4.15: Precategory-identity-system
- Theorem 9.4.16: Category-identity-system
9.5 The Yoneda lemma🔗
_ = _^op _ = _×ᶜ_ _ = Curry _ = Uncurry _ = Hom[-,-] _ = よ _ = よ-is-fully-faithful _ = Representation _ = Representation-is-prop _ = hom-iso→adjoints
- Definition 9.5.1: _^op
- Definition 9.5.2: _×ᶜ_
- Lemma 9.5.3: Curry,
Uncurry
- Corollary 9.5.6: よ-is-fully-faithful
- Corollary 9.5.7: As a corollary of Representation-is-prop
- Definition 9.5.8: Representation
- Theorem 9.5.9: Representation-is-prop
- Lemma 9.5.10:
hom-iso→adjoints
9.6 Strict categories🔗
This chapter is mostly text.
- Definition 9.6.1: Strict precategories
9.7 Dagger categories🔗
We do not have a type of dagger-categories, but note that we do have the closely-related notion of allegory.
9.8 The structure identity principle🔗
- Definition 9.8.1: Thin-structure-over, generalised into Displayed
- Theorem 9.8.2: Structured-objects-is-category, generalised into is-category-total
9.9 The Rezk completion🔗
_ = Rezk-completion-is-category _ = weak-equiv→pre-equiv _ = weak-equiv→pre-iso _ = eso→pre-faithful _ = eso-full→pre-ff _ = Rezk-completion _ = complete-is-eso _ = complete-is-ff _ = complete
- Lemma 9.9.1: eso→pre-faithful
- Lemma 9.9.2: eso-full→pre-ff
- Lemma 9.9.4: weak-equiv→pre-equiv, weak-equiv→pre-iso
- Theorem 9.9.5: Rezk-completion, Rezk-completion-is-category, complete, complete-is-ff, complete-is-eso.
Exercises🔗
_ = is-equivalence.F⁻¹⊣F _ = Total-space-is-eso _ = slice-is-category _ = Total-space-is-ff _ = Prebicategory _ = Total-space _ = Slice
- Exercise 9.1: Slice, slice-is-category
- Exercise 9.2: Total-space, Total-space-is-ff, Total-space-is-eso
- Exercise 9.3: is-equivalence.F⁻¹⊣F
- Exercise 9.4: Prebicategory
We use a slightly different definition of univalence for categories. It is shown equivalent to the usual formulation by
equiv-path→identity-system
↩︎