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.Material.HIT
open import Data.Set.Surjection
open import Data.Wellfounded.W
open import Data.Fin.Finite using (Listing→choice)
open import Data.Dec
open import Data.Nat using (ℕ-well-ordered ; Discrete-Nat)
open import Data.Sum

open import Homotopy.Space.Suspension.Freudenthal
open import Homotopy.Space.Suspension.Properties
open import Homotopy.Space.Sphere.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.Loopspace
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
_ = 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
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≃

Theorem 2.7.2: Σ-pathp≃
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
- 1. 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-contract
_ = Σ-contr-snd
_ = Σ-contr-fst

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-contract
Lemma 3.11.9: Σ-contr-snd, Σ-contr-fst

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-fst
_ = is-prop≃equiv∥-∥
_ = Listing→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-fst
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

Note

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:
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 $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

The pushout: Pushout
Definition 6.8.1: Cocone
Lemma 6.8.2: Pushout-is-universal-cocone
Observation: Susp≃pushout

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¹≃Int
_ = π₁S¹≅ℤ
_ = πₙ₊₂S¹≡0

Corollary 8.1.10: ΩS¹≃Int
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
_ = suspend-is-n-connected
_ = freudenthal.code
_ = freudenthal-equivalence
_ = Sⁿ-stability
_ = πₙSⁿ≃Int

Lemma 8.6.1: relative-n-type-const-plus
Lemma 8.6.2: Wedge.elim
Theorem 8.6.4: suspend-is-n-connected
Definition 8.6.5: freudenthal.code
Corollary 8.6.14: freudenthal-equivalence
Corollary 8.6.15: Sⁿ-stability
Theorem 8.6.17: πₙSⁿ≃Int

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 $Hom -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
- 1. empty-set
- 1. pairing
- 1. zero∈ℕ, suc∈ℕ
- 1. union
- 1. ∈-induction
- 1. replacement
- 1. separation

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