Homotopy Type Theory: Univalent Foundations of Mathematics N54F33XE07

URI	`m2://res/N54F33XE07`
Kind	textbook
Creators	The Univalent Foundations Program
Scope	deferred (no test decides the record, and the classifier has no model)

Expressions

e1: edition

Contents

chapter 1: Homotopy type theory
section 1.1: Types are higher groupoids
section 1.2: Functions are functors
section 1.3: Type families are fibrations
section 1.4: Homotopies and equivalences
section 1.5: The higher groupoid structure of type formers
section 1.6: Cartesian product types
section 1.7: \texorpdfstring{$\Sigma$}{Σ}-types
section 1.8: The unit type
section 1.9: \texorpdfstring{$\Pi$}{Π}-types and the function extensionality axiom
section 1.10: Universes and the univalence axiom
section 1.11: Identity type
section 1.12: Coproducts
section 1.13: Natural numbers
section 1.14: Example: equality of structures
subsection 1.14.1: Lifting equivalences
subsection 1.14.2: Equality of semigroups
section 1.15: Universal properties
chapter 2: Category theory
section 2.1: Categories and precategories
section 2.2: Functors and transformations
section 2.3: Adjunctions
section 2.4: Equivalences
section 2.5: The Yoneda lemma
section 2.6: Strict categories
section 2.7: \texorpdfstring{$\dagger$}{†}-categories
section 2.8: The structure identity principle
section 2.9: The Rezk completion
chapter 3: Equivalences
section 3.1: Quasi-inverses
section 3.2: Half adjoint equivalences
section 3.3: Bi-invertible maps
section 3.4: Contractible fibers
section 3.5: On the definition of equivalences
section 3.6: Surjections and embeddings
section 3.7: Closure properties of equivalences
section 3.8: The object classifier
section 3.9: Univalence implies function extensionality
chapter 4: Formal type theory
section: Preliminaries
section 4.1: The first presentation
subsection 4.1.1: Type universes
subsection 4.1.2: Dependent function types (\texorpdfstring{$\Pi$}{Π}-types)
subsection 4.1.3: Dependent pair types (\texorpdfstring{$\Sigma$}{Σ}-types)
subsection 4.1.4: Coproduct types
subsection 4.1.5: The finite types
subsection 4.1.6: Natural numbers
subsection 4.1.7: \texorpdfstring{$W$}{W}-types
subsection 4.1.8: Identity types
section 4.2: The second presentation
subsection 4.2.1: Contexts
subsection 4.2.2: Structural rules
subsection 4.2.3: Type universes
subsection 4.2.4: Dependent function types (\texorpdfstring{$\Pi$}{Π}-types)
subsection 4.2.5: Dependent pair types (\texorpdfstring{$\Sigma$}{Σ}-types)
subsection 4.2.6: Coproduct types
subsection 4.2.7: The empty type \texorpdfstring{$\emptyt$}{0}
subsection 4.2.8: The unit type \texorpdfstring{$\unit$}{1}
subsection 4.2.9: The natural number type
subsection 4.2.10: Identity types
subsection 4.2.11: Definitions
section 4.3: Homotopy type theory
subsection 4.3.1: Function extensionality and univalence
subsection 4.3.2: The circle
section 4.4: Basic metatheory
chapter 5: Higher inductive types
section 5.1: Introduction
section 5.2: Induction principles and dependent paths
section 5.3: The interval
section 5.4: Circles and spheres
section 5.5: Suspensions
section 5.6: Cell complexes
section 5.7: Hubs and spokes
section 5.8: Pushouts
section 5.9: Truncations
section 5.10: Quotients
section 5.11: Algebra
section 5.12: The flattening lemma
section 5.13: The general syntax of higher inductive definitions
chapter 6: Homotopy \texorpdfstring{$n$}{n}-types
section 6.1: Definition of \texorpdfstring{$n$}{n}-types
section 6.2: Uniqueness of identity proofs and Hedberg's theorem
section 6.3: Truncations
section 6.4: Colimits of \texorpdfstring{$n$}{n}-types
section 6.5: Connectedness
section 6.6: Orthogonal factorization
section 6.7: Modalities
chapter 7: Homotopy theory
section 7.1: \texorpdfstring{$\pi_1(S^1)$}{π₁(S¹)}
subsection 7.1.1: Getting started
subsection 7.1.2: The classical proof
subsection 7.1.3: The universal cover in type theory
subsection 7.1.4: The encode-decode proof
subsection 7.1.5: The homotopy-theoretic proof
subsection 7.1.6: The universal cover as an identity system
section 7.2: Connectedness of suspensions
section 7.3: \texorpdfstring{$\pi_{k \le n}$}{π\_(k≤n)} of an \texorpdfstring{$n$}{n}-connected space and \texorpdfstring{$\pi_{k < n}(\Sn ^n)$}{π\_(k<n)(Sⁿ)}
section 7.4: Fiber sequences and the long exact sequence
section 7.5: The Hopf fibration
subsection 7.5.1: Fibrations over pushouts
subsection 7.5.2: The Hopf construction
subsection 7.5.3: The Hopf fibration
section 7.6: The Freudenthal suspension theorem
section 7.7: The van Kampen theorem
subsection 7.7.1: Naive van Kampen
subsection 7.7.2: The van Kampen theorem with a set of basepoints
section 7.8: Whitehead's theorem and Whitehead's principle
section 7.9: A general statement of the encode-decode method
section 7.10: Additional Results
chapter 8: Induction
section 8.1: Introduction to inductive types
section 8.2: Uniqueness of inductive types
section 8.3: \texorpdfstring{$\w$}{W}-types
section 8.4: Inductive types are initial algebras
section 8.5: Homotopy-inductive types
section 8.6: The general syntax of inductive definitions
section 8.7: Generalizations of inductive types
section 8.8: Identity types and identity systems
chapter: Introduction
subsection: Type theory
subsection: Homotopy type theory
subsection: Univalent foundations
subsection: Higher inductive types
subsection: Sets in univalent foundations
subsection: Informal type theory
subsection: Constructivity
subsection: Open problems
subsection: How to read this book
chapter 9: Sets and logic
section 9.1: Sets and \texorpdfstring{$n$}{n}-types
section 9.2: Propositions as types?
section 9.3: Mere propositions
section 9.4: Classical vs.\ intuitionistic logic
section 9.5: Subsets and propositional resizing
section 9.6: The logic of mere propositions
section 9.7: Propositional truncation
section 9.8: The axiom of choice
section 9.9: The principle of unique choice
section 9.10: When are propositions truncated?
section 9.11: Contractibility
section: Notes
section: Exercises
part I: Foundations
part II: Mathematics
part: Appendix
chapter: Preface
subsection: IAS Special Year on Univalent Foundations
subsection: About this book
appendix A: Type theory
section A.1: Type theory versus set theory
section A.2: Function types
section A.3: Universes and families
section A.4: Dependent function types (\texorpdfstring{$\Pi$}{Π}-types)
section A.5: Product types
section A.6: Dependent pair types (\texorpdfstring{$\Sigma$}{Σ}-types)
section A.7: Coproduct types
section A.8: The type of booleans
section A.9: The natural numbers
section A.10: Pattern matching and recursion
section A.11: Propositions as types
section A.12: Identity types
subsection A.12.1: Path induction
subsection A.12.2: Equivalence of path induction and based path induction
subsection A.12.3: Disequality
appendix B: Real numbers
section B.1: The field of rational numbers
section B.2: Dedekind reals
subsection B.2.1: The algebraic structure of Dedekind reals
subsection B.2.2: Dedekind reals are Cauchy complete
subsection B.2.3: Dedekind reals are Dedekind complete
section B.3: Cauchy reals
subsection B.3.1: Construction of Cauchy reals
subsection B.3.2: Induction and recursion on Cauchy reals
subsection B.3.3: The algebraic structure of Cauchy reals
subsection B.3.4: Cauchy reals are Cauchy complete
section B.4: Comparison of Cauchy and Dedekind reals
section B.5: Compactness of the interval
section B.6: The surreal numbers
appendix C: Set theory
section C.1: The category of sets
subsection C.1.1: Limits and colimits
subsection C.1.2: Images
subsection C.1.3: Quotients
subsection C.1.4: \texorpdfstring{$\uset$}{Set} is a \texorpdfstring{$\Pi\mathsf{W}$}{ΠW}-pretopos
subsection C.1.5: The axiom of choice implies excluded middle
section C.2: Cardinal numbers
section C.3: Ordinal numbers
section C.4: Classical well-orderings
section C.5: The cumulative hierarchy
chapter: Index of symbols

Catalogue records

hott_book: hott_book (work)