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

## Chapter 3 Sets and Logic🔗

### 3.7 Propositional truncation🔗

The type itself is defined as a higher-inductive type ∥_∥. We also define as a shorthand for the truncation of Σ.

## Chapter 4 Equivalences🔗

### 4.4 Contractible fibres🔗

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

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

• The torus: .

### 6.10 Quotients🔗

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

# Part 2 Mathematics🔗

## Chapter 8 Homotopy theory🔗

The only non-trivial result worth mentioning from Chapter 8 is the fundamental group of the circle.

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

### Exercises🔗

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