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🔗

_ = sym
_ = _∙_
_ = ∙-idl
_ = ∙-idr
_ = ∙-invl
_ = ∙-invr
_ = ∙-assoc
_ = Ωⁿ⁺²-is-abelian-group
_ = Type∙
_ = Ωⁿ

• Lemma 2.1.1: sym
• Lemma 2.1.2: _∙_
• Lemma 2.1.4:
  1. ∙-idl, ∙-idr
  2. ∙-invl, ∙-invr
  3. Definitional in cubical type theory
  4. ∙-assoc
• Theorem 2.1.6: Ωⁿ⁺²-is-abelian-group
• Definition 2.1.7: Type∙
• Definition 2.1.8: Ωⁿ

2.2: Functions are functors🔗

_ = ap
_ = ap-∙

• 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🔗

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

• 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🔗

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

• 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🔗

_ = ⊎Path.Code≃Path

• Theorem 2.12.5: ⊎Path.Code≃Path

Exercises🔗

_ = Σ-assoc

• Exercise 2.10: Σ-assoc

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

• 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?🔗

_ = ¬DNE∞
_ = ¬LEM∞

• Theorem 3.2.2: ¬DNE∞
• Corollary 3.2.7: ¬LEM∞

3.3: Mere propositions🔗

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

• 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🔗

_ = LEM
_ = DNE
_ = Dec
_ = Discrete

• Definition 3.4.1: LEM
• Definition 3.4.2: DNE
• Definition 3.4.3:
  • 1. Dec
  • 3. Discrete

3.5: Subsets and propositional resizing🔗

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

• 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🔗

_ = Axiom-of-choice

• Definition 3.8.3: Axiom-of-choice

3.9: The principle of unique choice🔗

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

• 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🔗

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

• Definition 4.3.1: is-biinv
• Theorem 4.3.2: is-biinv-is-prop

4.4: Contractible fibres🔗

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

• 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:
  1. is-surjective
  2. is-embedding, embedding→cancellable
• 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🔗

_ = Fibre-equiv
_ = Total-equiv
_ = Map-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

• W-types: W

5.4: Inductive types are initial algebras🔗

_ = W-initial

• Theorem 5.4.7: W-initial

5.5: Homotopy-inductive types🔗

_ = initial→induction.elim

• Theorem 5.5.5: initial→induction.elim

Chapter 6: Higher inductive types🔗

6.2: Induction principles and dependent paths🔗

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

• 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🔗

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

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

• Lemma 6.3.1: interval-contractible

6.4: Circles and spheres🔗

_ = refl≠loop
_ = always-loop
_ = ap-square

• Lemma 6.4.1: refl≠loop
• Lemma 6.4.2: always-loop
• Lemma 6.4.4: ap-square

6.5: Suspensions🔗

_ = Susp
_ = SuspS⁰≡S¹
_ = Sⁿ⁻¹
_ = Σ-map∙≃map∙-Ω

• The suspension: Susp
• Lemma 6.5.1: SuspS⁰≡S¹
• Definition 6.5.2: Sⁿ⁻¹
• Lemma 6.5.4: Σ-map∙≃map∙-Ω

6.6: Cell complexes🔗

_ = T²

• The torus: T².

6.8: Pushouts🔗

_ = Pushout
_ = Cocone
_ = Pushout-is-universal-cocone
_ = Susp≡Pushout-⊤←A→⊤

• The pushout: Pushout
• Definition 6.8.1: Cocone
• Lemma 6.8.2: Pushout-is-universal-cocone
• Observation: Susp≡Pushout-⊤←A→⊤

6.9: Truncations🔗

_ = ∥-∥₀-elim

• Lemma 6.9.1: ∥-∥₀-elim

6.10: Quotients🔗

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

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

• Lemma 6.10.3: Coeq-univ.

6.11: Algebra🔗

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

• 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🔗

_ = T²≃S¹×S¹

• Exercise 6.3: T²≃S¹×S¹

Chapter 7: Homotopy n-types🔗

7.1: Definition of n-types🔗

_ = is-hlevel
_ = retract→is-hlevel
_ = Π-is-hlevel
_ = n-Type-is-hlevel

• 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🔗

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

• 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🔗

_ = is-n-connected≃∥-∥

• 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🔗

_ = Susp-is-connected
_ = Sⁿ⁻¹-is-connected

• Theorem 8.2.1: Susp-is-connected
• Corollary 8.2.2: Sⁿ⁻¹-is-connected

8.6: The Freudenthal suspension theorem🔗

_ = relative-n-type-const-plus
_ = Wedge.elim

• 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

Cat.Morphism, Cat.Univalent.

• 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.6¹: 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 and Nat-is-set
  • The one after that is Functor-path.
• 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 for Cat.
• Lemma 9.2.11: See the definition of Prebicategory.triangle for Cat.

9.3: Adjunctions🔗

_ = _⊣_
_ = is-left-adjoint-is-prop

• 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
  • The $\mathbf{Hom}\text{-functor:}$ Hom[-,-]
  • The Yoneda embedding: よ
• 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🔗

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

• Definition 9.8.1: Thin-structure-over, generalised into Displayed
• Theorem 9.8.2: Structured-objects-is-category, generalised into is-category-total

9.9: The Rezk completion🔗

_ = Rezk-completion-is-category
_ = weak-equiv→pre-equiv
_ = weak-equiv→pre-iso
_ = is-eso→precompose-is-faithful
_ = eso-full→pre-ff
_ = Rezk-completion
_ = complete-is-eso
_ = complete-is-ff
_ = complete

• Lemma 9.9.1: is-eso→precompose-is-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:
  • 1. extensionality
  • 2. empty-set
  • 3. pairing
  • 4. zero∈ℕ, suc∈ℕ
  • 22. union
  • 7. ∈-induction
  • 8. replacement
  • 9. separation