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🔗

2.2 Functions are functors🔗

  • Lemma 2.2.1: ap
  • Lemma 2.2.2:
    1. ap-comp-path
    2. Definitional in cubical type theory
    3. Definitional in cubical type theory
    4. Definitional in cubical type theory

2.3 Type families are fibrations🔗

2.4 Homotopies and equivalences🔗

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🔗

2.11 Identity type🔗

2.12 Coproducts🔗

Chapter 3 Sets and Logic🔗

3.1 Sets and n-types🔗

3.3 Mere propositions🔗

3.5 Subsets and propositional resizing🔗

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🔗

3.11 Contractibility🔗


Chapter 4 Equivalences🔗

4.2 Half adjoint equivalences🔗

4.3 Bi-invertible maps🔗

4.4 Contractible fibres🔗

Note: This is our “default” definition of equivalence, but we generally use it through the interface of half-adjoint equivalences.

4.8 The object classifier🔗

Chapter 6 Higher inductive types🔗

6.2 Induction principles and dependent paths🔗

6.3 The interval🔗

This is the higher inductive type [0,1], not the interval type I.

6.4 Circles and spheres🔗

6.6 Cell complexes🔗

_ = 
  • The torus: .

6.9 Truncations🔗

6.10 Quotients🔗

We define the quotient _/_ in terms of coequalisers Coeq.

6.11 Algebra🔗

Chapter 7 Homotopy n-types🔗

7.1 Definition of n-types🔗

7.2 Uniqueness of identity proofs and Hedberg’s theorem🔗

7.3 Truncations🔗

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

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.

9.2 Functors and Transformations🔗

9.3 Adjunctions🔗

9.4 Equivalences🔗

9.5 The Yoneda lemma🔗

9.6 Strict categories🔗

This chapter is mostly text.

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🔗

9.9 The Rezk completion🔗


  1. We use a slightly different definition of univalence for categories. It is shown equivalent to the usual formulation by equiv-path→identity-system↩︎