open import 1Lab.Equiv.Biinv

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

open import Cat.Instances.Sets.CartesianClosed
open import Cat.Instances.Sets.Congruences
open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Hom.Representable
open import Cat.Instances.Functor.Compose
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.Displayed.Univalence
open import Cat.Functor.Adjoint.Hom
open import Cat.Functor.Equivalence
open import Cat.Diagram.Congruence
open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Functor.Adjoint
open import Cat.Instances.Slice
open import Cat.Displayed.Base
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 Data.Set.Surjection
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.Circle
open import Homotopy.Space.Torus
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🔗

_ = sym
_ = _∙_
_ = ∙-id-l
_ = ∙-id-r
_ = ∙-inv-l
_ = ∙-inv-r
_ = ∙-assoc
_ = Ωⁿ⁺²-is-abelian-group
_ = Type∙
_ = Ωⁿ

2.2 Functions are functors🔗

_ = ap
_ = ap-comp-path
  • 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🔗

_ = subst
_ = Σ-pathp
_ = transport-refl
_ = subst-∙

2.4 Homotopies and equivalences🔗

_ = homotopy-natural
_ = homotopy-invert
_ = is-iso
_ = transport⁻transport
_ = id-equiv
_ = Equiv.inverse
_ = _∙e_

2.7 Cartesian product types🔗

_ = Σ-pathp-iso
  • Theorem 2.7.2: Σ-pathp-iso
  • Theorem 2.7.3: Agda has definitional η equality for records.

2.9 Π-types and function extensionality🔗

_ = funext
_ = funext-dep
  • Theorem 2.9.3: funext (no longer an axiom)
  • Lemma 2.9.6: funext-dep (no longer an axiom)

2.10 Universes and univalence🔗

_ = path→equiv
_ = 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

2.12 Coproducts🔗

_ = ⊎Path.Code≃Path

Chapter 3 Sets and Logic🔗

3.1 Sets and n-types🔗

_ = is-set
_ = Nat-is-set
_ = ×-is-hlevel
_ = Π-is-hlevel
_ = is-groupoid
_ = is-hlevel-suc

3.3 Mere propositions🔗

_ = is-prop
_ = prop-ext
_ = is-prop→is-set
_ = is-prop-is-prop
_ = is-hlevel-is-prop

3.5 Subsets and propositional resizing🔗

_ = Σ-prop-path
_ = Ω
_ = □

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🔗

_ = is-prop→equiv∥-∥
_ = ∥-∥-univ
_ = ∥-∥-proj

3.11 Contractibility🔗

_ = is-contr
_ = is-contr-is-prop
_ = retract→is-contr
_ = 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

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

4.3 Bi-invertible maps🔗

_ = is-biinv
_ = is-biinv-is-prop

4.4 Contractible fibres🔗

_ = is-equiv
_ = is-equiv→is-half-adjoint-equiv
_ = is-equiv-is-prop

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🔗

_ = Fibre-equiv
_ = Total-equiv
_ = Map-classifier

Chapter 6 Higher inductive types🔗

6.2 Induction principles and dependent paths🔗

_ = to-pathp
_ = from-pathp
_ = S¹-rec
_ = Ωⁿ≃Sⁿ-map

6.3 The interval🔗

_ = [0,1]
_ = I
_ = interval-contractible

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

6.4 Circles and spheres🔗

_ = refl≠loop

6.6 Cell complexes🔗

_ = T²
  • The torus: T².

6.9 Truncations🔗

_ = ∥-∥₀-elim

6.10 Quotients🔗

_ = Coeq
_ = _/_
_ = Coeq-univ

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

6.11 Algebra🔗

_ = Monoid-on
_ = Group-on
_ = πₙ₊₁
_ = Monoid.Free⊣Forget
_ = Group.make-free-group

Chapter 7 Homotopy n-types🔗

7.1 Definition of n-types🔗

_ = is-hlevel
_ = retract→is-hlevel
_ = Π-is-hlevel
_ = 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

7.3 Truncations🔗

_ = n-Tr-is-hlevel
_ = n-Tr-elim

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

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

Cat.Morphism, Cat.Univalent.

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

9.3 Adjunctions🔗

_ = _⊣_
_ = 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

9.5 The Yoneda lemma🔗

_ = _^op
_ = _×ᶜ_
_ = Curry
_ = Uncurry
_ = Hom[-,-]
_ = よ
_ = よ-is-fully-faithful
_ = Representation
_ = Representation-is-prop
_ = hom-iso→adjoints

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🔗

_ = Structured-objects-is-category
_ = is-category-total
_ = Thin-structure-over
_ = Displayed

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

Exercises🔗

_ = is-equivalence.F⁻¹⊣F
_ = Total-space-is-eso
_ = slice-is-category
_ = Total-space-is-ff
_ = Prebicategory
_ = Total-space
_ = Slice

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