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 _ = _∙_ _ = ∙-idl _ = ∙-idr _ = ∙-invl _ = ∙-invr _ = ∙-assoc _ = Ωⁿ⁺²-is-abelian-group _ = Type∙ _ = Ωⁿ
- Lemma 2.1.1:
sym
- Lemma 2.1.2:
_∙_
- Lemma 2.1.4:
- 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:
ap-∙
- Definitional in cubical type theory
- Definitional in cubical type theory
- 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🔗
_ = homotopy-natural _ = homotopy-invert _ = is-iso _ = transport⁻transport _ = id-equiv _ = Equiv.inverse _ = _∙e_
- 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🔗
_ = is-equiv→is-embedding _ = subst-path-left _ = subst-path-right _ = transport-path _ = commutes→square
- 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?🔗
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🔗
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
,∥-∥-out
3.11: Contractibility🔗
_ = is-contr _ = is-contr-is-prop _ = retract→is-contr _ = Singleton-is-contr _ = Σ-contract _ = Σ-contr-eqv
- 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🔗
_ = equiv→is-hlevel _ = ⊎-is-hlevel _ = Σ-is-hlevel _ = is-contr-if-inhabited→is-prop _ = is-prop∙→is-contr _ = H-Level-Dec _ = disjoint-⊎-is-prop _ = ¬global-choice _ = ∥-∥-elim _ = LEM≃DNE _ = ℕ-well-ordered _ = Σ-contr-eqv _ = is-prop≃equiv∥-∥ _ = Finite-choice
- 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🔗
_ = 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
- 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🔗
This is our “default” definition of equivalence, but we generally use it through the interface of half-adjoint equivalences.
- 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🔗
_ = is-surjective _ = is-embedding _ = embedding→cancellable _ = injective _ = is-equiv→is-surjective _ = is-equiv→is-embedding _ = embedding-surjective→is-equiv
- Definition 4.6.1:
- 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 : by pattern matching.
- Lemma 6.2.5:
S¹-rec
- Lemma 6.2.9:
Ωⁿ≃Sⁿ-map
forn = 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.8: Pushouts🔗
- The pushout:
Pushout
- Definition 6.8.1:
Cocone
- Lemma 6.8.2:
Pushout-is-universal-cocone
- Observation:
Susp≡Pushout-⊤←A→⊤
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-monoid⊣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🔗
_ = set-identity-system _ = identity-system→hlevel _ = Discrete→is-set _ = Discrete-Nat _ = hubs-and-spokes→hlevel _ = hlevel→hubs-and-spokes
- 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🔗
_ = is-n-connected _ = is-n-connected-Tr _ = relative-n-type-const _ = is-n-connected→n-type-const _ = n-type-const→is-n-connected _ = is-n-connected-point _ = point-is-n-connected
- 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¹)🔗
_ = S¹Path.Cover _ = S¹Path.encode _ = S¹Path.decode _ = S¹Path.encode-decode _ = S¹Path.encode-loopⁿ _ = ΩS¹≃integers _ = π₁S¹≡ℤ _ = πₙ₊₂S¹≡0
- 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🔗
_ = Precategory _ = is-invertible _ = _≅_ _ = is-invertible-is-prop _ = Cat[_,_] _ = path→iso _ = is-category _ = equiv-path→identity-system _ = Univalent.Ob-is-groupoid _ = Hom-transport _ = path→to-sym _ = path→to-∙ _ = Poset _ = is-gaunt _ = Disc _ = Rel _ = Sets _ = Sets-is-category
- Definition 9.1.1:
Precategory
- Definition 9.1.2:
is-invertible
,_≅_
- Lemma 9.1.3:
is-invertible-is-prop
- Lemma 9.1.4:
path→iso
- Example 9.1.5:
Sets
- Definition 9.1.61:
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🔗
_ = Functor _ = _=>_ _ = Nat-is-set _ = Functor-path _ = invertible→invertibleⁿ _ = isoⁿ→iso _ = Functor-is-category _ = _F∘_ _ = _◂_ _ = _▸_ _ = F∘-assoc _ = Prebicategory.pentagon _ = Prebicategory.triangle _ = Cat
- Definition 9.2.1:
Functor
- Definition 9.2.2:
_=>_
- The paragraph immediately after 9.2.2 is
Nat-pathp
andNat-is-set
- The one after that is
Functor-path
.
- The paragraph immediately after 9.2.2 is
- 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
forCat
. - Lemma 9.2.11: See the definition of
Prebicategory.triangle
forCat
.
9.3: Adjunctions🔗
- Lemma 9.3.1:
_⊣_
- Lemma 9.3.2:
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
- 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🔗
_ = _^op _ = _×ᶜ_ _ = Curry _ = Uncurry _ = Hom[-,-] _ = よ _ = よ-is-fully-faithful _ = Representation _ = Representation-is-prop _ = hom-iso→adjoints
- Definition 9.5.1:
_^op
- Definition 9.5.2:
_×ᶜ_
- Lemma 9.5.3:
Curry
,Uncurry
- 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 intoDisplayed
- Theorem 9.8.2:
Structured-objects-is-category
, generalised intois-category-total
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
- 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🔗
_ = is-equivalence.F⁻¹⊣F _ = Total-space-is-eso _ = slice-is-category _ = Total-space-is-ff _ = Prebicategory _ = Total-space _ = Slice
- 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🔗
_ = Sets-is-complete _ = Sets-is-cocomplete _ = Sets-regular _ = surjective→regular-epi _ = epi→surjective _ = Sets-effective-congruences _ = Congruence.is-effective _ = Susp-prop-is-set _ = Susp-prop-path _ = AC→LEM
- 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🔗
_ = V _ = presentation _ = Presentation.members _ = extensionality _ = empty-set _ = pairing _ = zero∈ℕ _ = suc∈ℕ _ = union _ = ∈-induction _ = replacement _ = separation
- Definition 10.5.1:
V
- Lemma 10.5.6:
presentation
- Definition 10.5.7:
Presentation.members
- Theorem 10.5.8:
We use a slightly different definition of univalence for categories. It is shown equivalent to the usual formulation by
equiv-path→identity-system
↩︎