open import 1Lab.Counterexamples.GlobalChoice
open import 1Lab.Function.Surjection
open import 1Lab.Function.Embedding
open import 1Lab.Equiv.Biinv
open import 1Lab.Classical

open import Algebra.Group.Homotopy
open import Algebra.Monoid
open import Algebra.Group

open import Cat.Instances.Sets.Congruences
open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Hom.Representable
open import Cat.Instances.Sets.Cocomplete
open import Cat.Functor.Equivalence.Path
open import Cat.Univalent.Rezk.Universal
open import Cat.Instances.Sets.Complete
open import Cat.Functor.Adjoint.Unique
open import Cat.Regular.Instances.Sets
open import Cat.Displayed.Univalence
open import Cat.Functor.Adjoint.Hom
open import Cat.Functor.Equivalence
open import Cat.Diagram.Congruence
open import Cat.Functor.Properties
open import Cat.Instances.Discrete
open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Functor.Adjoint
open import Cat.Functor.Compose
open import Cat.Instances.Slice
open import Cat.Displayed.Base
open import Cat.Functor.Closed
open import Cat.Instances.Sets
open import Cat.Univalent.Rezk
open import Cat.Allegory.Base
open import Cat.Functor.Base
open import Cat.Functor.Hom
open import Cat.Univalent
open import Cat.Morphism
open import Cat.Bi.Base
open import Cat.Prelude
open import Cat.Gaunt

open import Data.Set.Surjection
open import Data.Wellfounded.W
open import Data.Set.Material
open import Data.Fin.Finite using (Finite-choice)
open import Data.Dec
open import Data.Nat using (ℕ-well-ordered ; Discrete-Nat)
open import Data.Sum

open import Homotopy.Space.Suspension.Properties
open import Homotopy.Space.Suspension
open import Homotopy.Connectedness
open import Homotopy.Space.Circle
open import Homotopy.Space.Sphere
open import Homotopy.Space.Torus
open import Homotopy.Truncation
open import Homotopy.Pushout
open import Homotopy.Wedge
open import Homotopy.Base

open import Order.Base

import Algebra.Monoid.Category as Monoid
import Algebra.Group.Free as Group
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-∙
    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🔗

Exercises🔗

Chapter 3: Sets and Logic🔗

3.1: Sets and n-types🔗

3.2: Propositions as types?🔗

3.3: Mere propositions🔗

3.4: Classical vs. intuitionistic logic🔗

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

3.9: The principle of unique choice🔗

3.11: Contractibility🔗

Exercises🔗

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

4.8: The object classifier🔗

Chapter 5: Induction🔗

5.3: W-types🔗

_ = W
  • W-types: W

5.4: Inductive types are initial algebras🔗

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.5: Suspensions🔗

6.6: Cell complexes🔗

_ = 
  • The torus: .

6.8: Pushouts🔗

6.9: Truncations🔗

6.10: Quotients🔗

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

6.11: Algebra🔗

Exercises🔗

Chapter 7: Homotopy n-types🔗

7.1: Definition of n-types🔗

7.2: Uniqueness of identity proofs and Hedberg’s theorem🔗

7.3: Truncations🔗

7.5: Connectedness🔗

Exercises🔗

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

8.2: Connectedness of suspensions🔗

8.6: The Freudenthal suspension theorem🔗

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🔗

Exercises🔗

Chapter 10: Set theory🔗

10.1: The category of sets🔗

10.5: The cumulative hierarchy🔗


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