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🔗

• Lemma 2.1.1: sym
• Lemma 2.1.2: _∙_
• Lemma 2.1.4:
  1. ∙-idl, ∙-idr
  2. ∙-invl, ∙-invr
  3. Definitional in cubical type theory
  4. ∙-assoc
• 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:
  1. ap-∙
  2. Definitional in cubical type theory
  3. Definitional in cubical type theory
  4. 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🔗

• 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🔗

• 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

Exercises🔗

• Exercise 2.10: Σ-assoc

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.2 Propositions as types?🔗

• Theorem 3.2.2: ¬DNE∞
• Corollary 3.2.7: ¬LEM∞

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.4 Classical vs. intuitionistic logic🔗

• Definition 3.4.1: LEM
• Definition 3.4.2: DNE
• Definition 3.4.3:
  1. Dec
  2. Discrete

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.8 The axiom of choice🔗

• Definition 3.8.3: Axiom-of-choice

3.9 The principle of unique choice🔗

• Lemma 3.9.1: is-prop→equiv∥-∥
• Corollary 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
• Lemma 3.11.9: Σ-contract, Σ-contr-eqv

Exercises🔗

• Exercise 3.1: equiv→is-hlevel
• Exercise 3.2: ⊎-is-hlevel
• Exercise 3.3: Σ-is-hlevel
• Exercise 3.5: is-contr-if-inhabited→is-prop, is-prop∙→is-contr
• Exercise 3.6: H-Level-Dec
• Exercise 3.7: disjoint-⊎-is-prop
• Exercise 3.11: ¬global-choice
• Exercise 3.17: ∥-∥-elim
• Exercise 3.18: LEM≃DNE
• Exercise 3.19: ℕ-well-ordered
• Exercise 3.20: Σ-contr-eqv
• Exercise 3.21: is-prop≃equiv∥-∥
• Exercise 3.22: Finite-choice

Chapter 4 Equivalences🔗

4.2 Half adjoint equivalences🔗

• 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🔗

• 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.6 Surjections and embeddings🔗

• Definition 4.6.1:
  1. is-surjective
  2. is-embedding, embedding→cancellable
• Definition 4.6.2: injective
• Theorem 4.6.3: is-equiv→is-surjective, is-equiv→is-embedding, embedding-surjective→is-equiv

4.8 The object classifier🔗

• Lemma 4.8.1: Fibre-equiv
• Lemma 4.8.2: Total-equiv
• Theorem 4.8.3: Map-classifier

Chapter 5 Induction🔗

5.3 W-types🔗

• W-types: W

5.4 Inductive types are initial algebras🔗

• Theorem 5.4.7: W-initial

Chapter 6 Higher inductive types🔗

6.2 Induction principles and dependent paths🔗

• Remark 6.2.3: to-pathp, from-pathp
• _Induction principle for $\mathbb{S}^1$: 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
• Lemma 6.4.2: always-loop
• Lemma 6.4.4: ap-square

6.5 Suspensions🔗

• The suspension: Susp
• Lemma 6.5.1: SuspS⁰≡S¹
• Definition 6.5.2: Sⁿ⁻¹
• Lemma 6.5.4: Σ-map∙≃map∙-Ω

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

Exercises🔗

• Exercise 6.3: T²≃S¹×S¹

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🔗

• 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

7.5 Connectedness🔗

• Definition 7.5.1: is-n-connected, is-n-connected-Tr
• Lemma 7.5.7: relative-n-type-const
• Corollary 7.5.9: is-n-connected→n-type-const, n-type-const→is-n-connected
• Lemma 7.5.11: is-n-connected-point, point-is-n-connected

Exercises🔗

• Exercise 7.6: is-n-connected≃∥-∥

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¹)🔗

• 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
• Corollary 8.1.11: π₁S¹≡ℤ, πₙ₊₂S¹≡0

8.2 Connectedness of suspensions🔗

• Theorem 8.2.1: Susp-is-connected
• Corollary 8.2.2: Sⁿ⁻¹-is-connected

8.6 The Freudenthal suspension theorem🔗

• Lemma 8.6.1: relative-n-type-const-plus
• Lemma 8.6.2: Wedge.elim

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🔗

Cat.Morphism, Cat.Univalent.

• 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
• Example 9.1.5: Sets
• Definition 9.1.6¹: 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.15: is-gaunt
• Example 9.1.16: Disc
• Example 9.1.19: Rel

9.2 Functors and Transformations🔗

• 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: invertible→invertibleⁿ; Only if: 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🔗

• 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🔗

• Definition 9.5.1: _^op
• Definition 9.5.2: _×ᶜ_
• Lemma 9.5.3: Curry, Uncurry
  • The $\mathbf{Hom}$-functor: Hom[-,-]
  • The Yoneda embedding: よ
• 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: Adjoints in terms of representability

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🔗

• 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🔗

• 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

Chapter 10 Set theory🔗

10.1 The category of sets🔗

• 10.1.1 Limits and colimits: Sets-is-complete, Sets-is-cocomplete
• Theorem 10.1.5: Sets-regular, surjective→regular-epi, epi→surjective
• 10.1.3 Quotients: Sets-effective-congruences
• Lemma 10.1.8: Congruence.is-effective
• Lemma 10.1.13: Susp-prop-is-set, Susp-prop-path
• Theorem 10.1.14: AC→LEM

10.5 The cumulative hierarchy🔗

• Definition 10.5.1: V
• Lemma 10.5.6: presentation
• Definition 10.5.7: Presentation.members
• Theorem 10.5.8:
  1. extensionality
  2. empty-set
  3. pairing
  4. zero∈ℕ, suc∈ℕ
  5. union
  6. ∈-induction
  7. replacement
  8. separation