Math 2.0

Resources / textbook

Homotopy Type Theory: Univalent Foundations of Mathematics N54F33XE07

URIm2://res/N54F33XE07
Kindtextbook
CreatorsThe Univalent Foundations Program
Date2026-05-12
MSC03B38, 55U35
Scopein

Expressions

e1: edition

Languageen
Date2026-05-12
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

Items in this resource

The mentions of the inventory that name this resource. Each name links to the card of its inventory row.

ItemKindWhereSource
integers, induction principle forconceptindex, section 5.10hott_book
generator, of a groupconceptindex, section 7.7.2hott_book
11K8HRD7HFstatementlem, section B.4hott_book
11QPK3AYNHexerciseex, section 9.11hott_book
122EKTGN1Hproofproof, section 3.7hott_book
judgmental equalityconceptindex, section sec:formal-prelimhott_book
uniqueness, of identity typesconceptindex, section 8.2hott_book
13CA73DK6Fdefinitiondefn, section 9.1hott_book
146VJYCF6Xstatementlem, section 6.2hott_book
1558F7ATJFstatementthm, section 8.8hott_book
15QKRXFNGNproofproof, section C.1.2hott_book
introduction ruleconceptindex, section 4.2.4hott_book
transport, in function typesconceptindex, section 1.9hott_book
16DP25MPY3definitiondefn, section 3.6hott_book
16ERV9K3HQstatementthm, section 3.2hott_book
unit, of a ringconceptindex, section B.2.1hott_book
17KSNDXK1Fstatementthm, section C.1.5hott_book
universal, property, of metric completionconceptindex, section B.6hott_book
induction principle, for homotopiesconceptindex, section 8.8hott_book
computation rule, for higher inductive typesconceptindex, section 5.2hott_book
induction principle, for torusconceptindex, section 5.6hott_book
encode-decode methodconceptindex, section 7.6hott_book
recursion principle, for cartesian productconceptindex, section A.5hott_book
axiom, of choiceconceptindex, section 2hott_book
theorem, Cantor'sconceptindex, section C.2hott_book
octahedral axiom, unstableconceptindex, section 3.9hott_book
1AJ4MSJKENproofproof, section 3.9hott_book
1B4SVCV2MDstatementthm, section 6.6hott_book
axiom, unstable octahedralconceptindex, section 3.9hott_book
successorconceptindex, section 8.3hott_book
1BEDC424EAstatementlem, section 3.2hott_book
universal, property, of $\Sn^1$conceptindex, section 5.2hott_book
1CTJZ19DBPexerciseex, section A.12.3hott_book
open, problemconceptindex, section u1.u8hott_book
1CZDTYNNAZstatementlem, section C.4hott_book
1DDA60E4TCexampleeg, section 7.7.1hott_book
free, generation of an inductive typeconceptindex, section 5.1hott_book
1DZEY5B6EAstatementcor, section 2.5hott_book
Path lifting propertystatementlem, section 1.3hott_book
$n$-typeconceptindex, section 9.1hott_book
type, dependent pairconceptindex, section 1.7hott_book
type, circleconceptindex, section 5.5hott_book
ordinalconceptindex, section C.3hott_book
successor, of an ordinalconceptindex, section C.5hott_book
1FM2SG3JSPstatementthm, section B.3.2hott_book
1G2SPBJH3Xstatementlem, section 1.9hott_book
1G4GHAHSFFstatementlem, section 9.11hott_book
1G9QW9HCA0proofproof, section B.3.3hott_book
pseudo-ordinalconceptindex, section B.6hott_book
1HATHFDXS3proofproof, section B.3.2hott_book
1HKTEYFKVAproofproof, section 5.5hott_book
1JB263SJGZproofproof, section 2.5hott_book
helixconceptindex, section 7.1.2hott_book
toposconceptindex, section Chott_book
path, 2-conceptindex, section 1.1hott_book
addition, of surreal numbersconceptindex, section B.6hott_book
homotopy, groupconceptindex, section 5.11hott_book
fundamental, $\infty$-groupoidconceptindex, section 1hott_book
transitivity, of $<$ for realsconceptindex, section B.2.1hott_book
uniqueness, principleconceptindex, section A.12.3hott_book
initial, segmentconceptindex, section C.3hott_book
induction principle, for equivalencesconceptindex, section 8.8hott_book
universal, coverconceptindex, section 7.1.3hott_book
1Q9XS6JGM1statementcor, section 3.3hott_book
proof, assistantconceptindex, section 4hott_book
1QVWHPYJ28proofproof, section 6.3hott_book
1SAHQFSPW0statementthm, section 3.7hott_book
universal, property, of Rezk completionconceptindex, section 2.9hott_book
axiom, of choiceconceptindex, section u1.u7hott_book
Hedbergstatementthm, section 6.2hott_book
induction principle, for identity typeconceptindex, section A.12.1hott_book
1XKNMCRR31statementlem, section 2.3hott_book
1YTK7SC7TXproofproof, section 2.2hott_book
1Z13P4H7KRstatementlem, section 3.8hott_book
automorphism, of $\Sn^1$conceptindex, section 5.4hott_book
$\Pi\mathsfW$-pretoposconceptindex, section C.1.4hott_book
1ZKSYDG4XNstatementlem, section 5.2hott_book
hypothesis, inductiveconceptindex, section A.9hott_book
membershipconceptindex, section A.1hott_book
excluded middleconceptindex, section 9.2hott_book
topological, pathconceptindex, section 1hott_book
fiberwise, $n$-connected family of functionsconceptindex, section 6.5hott_book
Second proofproofproof, section 1.1hott_book
22HM7RAF98exerciseex, section 8.8hott_book
evidence, of the truth of a propositionconceptindex, section A.1hott_book
type, circleconceptindex, section 4.3.2hott_book
248BVX8RZ2proofproof, section C.2hott_book
presentation, of an $\infty$-groupoidconceptindex, section 7hott_book
Whitehead's, theoremconceptindex, section 7.8hott_book
total, spaceconceptindex, section 3.7hott_book
generation, of a type, inductiveconceptindex, section A.12.1hott_book
252S9HDJPYstatementthm, section B.2.1hott_book
fiber sequenceconceptindex, section 7.4hott_book
25KCN3FKNTexerciseex, section 9.11hott_book
263F2E10TRproofproof, section 7.6hott_book
model categoryconceptindex, section u1.u2hott_book
uniqueness, principle, for dependent function typesconceptindex, section A.4hott_book
26KVPJPRSXdefinitiondefn, section 6.7hott_book
extraction of algorithmsconceptindex, section u1.u7hott_book
275PCM1VVNexerciseex, section 2.9hott_book
28BXFHG0DQproofproof, section 7.2hott_book
28HMFCW06Eproofproof, section B.4hott_book
set theory, Zermelo--Fraenkelconceptindex, section A.1hott_book
depressionconceptindex, section B.5hott_book
proof, assistantconceptindex, section u1.u6hott_book
pushoutconceptindex, section 7.10hott_book
path, 2-conceptindex, section 1hott_book
accessibilityconceptindex, section C.3hott_book
2B6N4T0GSBproofproof, section 3.7hott_book
Cauchy, sequenceconceptindex, section B.5hott_book
compactness, Bolzano--Weierstra\ssconceptindex, section B.5hott_book
2CXM9MST8Yexerciseex, section 1.15hott_book
adjoint, functorconceptindex, section 1.15hott_book
2DM84ZX34Hproofproof, section 9.2hott_book
2DWZQTDVC1statementlem, section 7.4hott_book
induction principleconceptindex, section 4.2.4hott_book
2F94YK8FVHstatementlem, section 3.8hott_book
variableconceptindex, section A.2hott_book
bijectionconceptindex, section 1.4hott_book
uniqueness, principle, propositional, for product typesconceptindex, section A.5hott_book
2GWE0X51NJexerciseex, section 6.7hott_book
2GXZNN4D0Xdefinitiondefn, section 2.2hott_book
2H1N36TAFBstatementlem, section B.3.2hott_book
type theoryconceptindex, section A.1hott_book
2JRPX292CTexerciseex, section 1.15hott_book
2JT5ENJM14exerciseex, section 1.15hott_book
path, 3-conceptindex, section 1hott_book
faithful functorconceptindex, section 2.4hott_book
2KFD4VTJA0proofproof, section C.3hott_book
2KKA91SYHHproofproof, section C.4hott_book
globular operadconceptindex, section 1.1hott_book
2M8P8QEBYQdefinitiondefn, section 7.4hott_book
2MKBG0H264exerciseex, section B.6hott_book
$\w$-type, impredicative encoding ofconceptindex, section 8.8hott_book
cardinal number, inequality ofconceptindex, section C.2hott_book
2PMD455T0Zexampleeg, section 7.7.2hott_book
completion, exactconceptindex, section C.1.4hott_book
2QB6N126EQexerciseex, section 7.10hott_book
Cauchy, approximationconceptindex, section B.5hott_book
2QPN5HS655exampleeg, section 2.1hott_book
fixed-point propertyconceptindex, section 8.8hott_book
order, strictconceptindex, section B.6hott_book
type, coproductconceptindex, section 1.12hott_book
2SCTZQBCQAstatementcor, section 1.7hott_book
simplicity theoremconceptindex, section B.6hott_book
2TRMECF5EPstatementthm, section B.2.2hott_book
2TVP0TP1J8definitiondefn, section 8.8hott_book
2TYH9G1HKRexerciseex, section 2.9hott_book
2TZ62Y41Q3statementlem, section 7.5.3hott_book
2TZXXKJCYAexerciseex, section C.5hott_book
logic, propositions as typesconceptindex, section A.11hott_book
2VK093MWF2proofproof, section 6.2hott_book
2VVFMCNKJ3proofproof, section 9.3hott_book
open, relationconceptindex, section B.3.2hott_book
2WRKS9ABADexerciseex, section 2.9hott_book
Homotopy inductionstatementcor, section 8.8hott_book
2XNGWZ7QH4statementlem, section B.3.2hott_book
2Y558QSZETproofproof, section 7.8hott_book
2Y6THFBWQ5proofproof, section 3.4hott_book
cone, of a functionconceptindex, section C.1.2hott_book
2ZEWHTG6ADstatementthm, section B.2.1hott_book
$\lambda$-abstractionconceptindex, section 4.1hott_book
3012J5E2M5statementthm, section 8.4hott_book
30EFJC9ACAproofproof, section 2.5hott_book
30W8SPKMVYstatementlem, section C.2hott_book
31CKFRXF8Yproofproof, section 5.5hott_book
ZF-algebraconceptindex, section C.5hott_book
complete, categoryconceptindex, section C.1.1hott_book
path, inductionconceptindex, section A.12.1hott_book
cotransitivity of apartnessconceptindex, section B.2.1hott_book
relation, monotonicconceptindex, section B.3.2hott_book
set theory, Zermelo--Fraenkelconceptindex, section 5.11hott_book
Elementary Theory of the Category of Setsconceptindex, section Chott_book
order, strictconceptindex, section B.3.3hott_book
rule, structuralconceptindex, section 4.2.2hott_book
theory, essentially algebraicconceptindex, section 5.11hott_book
36FNQHVSZJproofproof, section 7.1.4hott_book
power setconceptindex, section C.1.3hott_book
coercion, universe-raisingconceptindex, section A.12.3hott_book
385M1V9Z14exerciseex, section A.12.3hott_book
38P7Y4F24Nstatementthm, section 1.15hott_book
initial, ordered fieldconceptindex, section B.1hott_book
Abstract Stone Dualityconceptindex, section B.6hott_book
natural, transformationconceptindex, section 3.1hott_book
mere propositionconceptindex, section 9.3hott_book
3B4D5HZM28definitiondefn, section 6.5hott_book
contractible, functionconceptindex, section 3.4hott_book
universe levelconceptindex, section 2hott_book
toposconceptindex, section C.1.4hott_book
3CT2HVA52Wstatementlem, section 6.6hott_book
3DGN2T3V2Mdefinitiondefn, section 2.2hott_book
3DQAWX07DXproofproof, section 1.10hott_book
3DW33PW1V4proofproof, section 6.7hott_book
3EKV5ATT07statementlem, section 7.1.5hott_book
3END89ECTYstatementthm, section 5.10hott_book
loop space, iteratedconceptindex, section 5.5hott_book
3GX4F6H7B7exampleeg, section 7.7.2hott_book
setconceptindex, section 5.9hott_book
3H5R8MYBFXstatementlem, section C.5hott_book
3HJWXE489Xdefinitiondefn, section 2.5hott_book
encode-decode methodconceptindex, section B.3.2hott_book
Wedge connectivity lemmastatementlem, section 7.6hott_book
evidence, of the truth of a propositionconceptindex, section A.11hott_book
3J8HJB96GYstatementthm, section 6.3hott_book
predecessorconceptindex, section 8.1hott_book
axiom, of choiceconceptindex, section 9.11hott_book
sequence, exactconceptindex, section 7.5hott_book
homotopy, (pre)category of typesconceptindex, section 2.9hott_book
3KJ9Q49SC3definitiondefn, section 6.4hott_book
associativity, of semigroup operationconceptindex, section 1.14hott_book
$\beta $-reductionconceptindex, section A.5hott_book
unique, choiceconceptindex, section 9.9hott_book
3MK5DWXDYZdefinitiondefn, section B.5hott_book
endofunctor, algebra forconceptindex, section 8.8hott_book
type, of listsconceptindex, section 8.3hott_book
fibrationconceptindex, section 1.3hott_book
3PSH0TRXFTproofproof, section 7.6hott_book
3PYGSVJCJKstatementlem, section 2.4hott_book
cut, Dedekindconceptindex, section B.2hott_book
3Q7Q4E4JWNproofproof, section 5.12hott_book
3QNCMJC2WYexampleeg, section 1.4hott_book
3REQNX2F68statementlem, section 6.5hott_book
induction principle, for truncationconceptindex, section 5.9hott_book
3RM5PG6G0Vstatementlem, section 9.9hott_book
3RMMSAJ7X1statementlem, section C.3hott_book
$(\infty,1)$-categoryconceptindex, section 8.4hott_book
functor, equivalenceconceptindex, section 2.4hott_book
3SVE8RZ0ZPproofproof, section C.5hott_book
3TEAAQEYDVproofproof, section 1.15hott_book
3TQMQC956Zstatementlem, section 3.4hott_book
adjoint, equivalenceconceptindex, section 1.4hott_book
transport, in dependent pair typesconceptindex, section 1.7hott_book
3XKZMCX44Vstatementlem, section 7.5.3hott_book
3XYMFMZGH8exerciseex, section C.5hott_book
Elementary Theory of the Category of Setsconceptindex, section u1.u5hott_book
type, intervalconceptindex, section 5.3hott_book
pathconceptindex, section 1hott_book
excluded middleconceptindex, section C.4hott_book
3Z86VZSRG3proofproof, section 3.8hott_book
40BACBTHHCproofproof, section 6.3hott_book
40FMKB38H3exampleeg, section 5.11hott_book
uniqueness, principle, propositional, for functions on the circleconceptindex, section 5.2hott_book
40TXB84P26statementthm, section 3.7hott_book
417A923EDXstatementlem, section 7.3hott_book
vertex of a coconeconceptindex, section 5.8hott_book
43Q8SH2G14statementthm, section B.5hott_book
loop space, iteratedconceptindex, section 6.3hott_book
function, identityconceptindex, section 1.10hott_book
basepoint, set ofconceptindex, section 7.7.2hott_book
454YEXPPYMstatementlem, section 1.9hott_book
equals may be substituted for equalsconceptindex, section A.12hott_book
loop spaceconceptindex, section 5.11hott_book
Blakers--Massey theoremstatementthm, section 7.10hott_book
merelyconceptindex, section 6.7hott_book
46ET0B5YNYexerciseex, section C.5hott_book
attaching mapconceptindex, section 5.7hott_book
variableconceptindex, section A.11hott_book
total, spaceconceptindex, section 7.1.5hott_book
480XTGXEXAproofproof, section 2.2hott_book
function, continuousconceptindex, section B.3.2hott_book
48JDCCHX7Cproofproof, section 7.8hott_book
topology, formalconceptindex, section B.5hott_book
logic, constructive vs classicalconceptindex, section u1.u7hott_book
4AG6MAF72Bproofproof, section B.2.1hott_book
mathematics, constructiveconceptindex, section B.2.1hott_book
4BQNFGDAZRproofproof, section 3.7hott_book
4BVVXMJ5VBexerciseex, section 3.9hott_book
presentation, of a groupconceptindex, section 7.7.2hott_book
4CWV59JPWHexerciseex, section 1.15hott_book
4CYG2TBEKPproofproof, section 6.4hott_book
retract, of a functionconceptindex, section 3.7hott_book
variable, typeconceptindex, section 8.6hott_book
abuse, of notationconceptindex, section 1.14hott_book
strict, orderconceptindex, section B.6hott_book
mathematics, classicalconceptindex, section u1.u7hott_book
4ERYCJ39TDproofproof, section 9.11hott_book
free, generation of an inductive typeconceptindex, section 8.8hott_book
4FWN0WES34statementlem, section 7.5.3hott_book
encode-decode methodconceptindex, section 7.1.4hott_book
4GFNY8FTXXproofproof, section 6.1hott_book
presentation, of a space as a CW complexconceptindex, section u1.u4hott_book
mathematics, proof-relevantconceptindex, section A.1hott_book
Lawvereconceptindex, section C.1.5hott_book
type theory, extensionalconceptindex, section A.12.3hott_book
monoidconceptindex, section 5.11hott_book
4JV78W2WX1statementcor, section 7.8hott_book
axiom, of choiceconceptindex, section 9.8hott_book
inductive-inductive type, higherconceptindex, section B.3.1hott_book
4MD82ZR9E9statementlem, section 7.7.2hott_book
definition, by pattern matchingconceptindex, section A.10hott_book
mathematics, formalizedconceptindex, section 3.5hott_book
4NMN9YJF4Sproofproof, section 1.7hott_book
4NQCGP23DGproofproof, section C.5hott_book
type, $n$-sphereconceptindex, section 7.6hott_book
induction principle, for surreal numbersconceptindex, section B.6hott_book
mathematics, classicalconceptindex, section C.3hott_book
suspensionconceptindex, section 5.8hott_book
4Q1G1CW3CDproofproof, section 6.3hott_book
contextconceptindex, section A.1hott_book
4QAQQX3WTKstatementthm, section B.5hott_book
encode-decode methodconceptindex, section C.1.3hott_book
interchange lawconceptindex, section 1.1hott_book
mathematics, formalizedconceptindex, section 7hott_book
type, higher inductiveconceptindex, section u1.u4hott_book
type, emptyconceptindex, section 4.2.7hott_book
acceptanceconceptindex, section 7hott_book
4TEZS81DT4proofproof, section 2.2hott_book
limit, of typesconceptindex, section 5.8hott_book
4V7TBEK7Z4exerciseex, section 8.8hott_book
mathematics, constructiveconceptindex, section Bhott_book
exact sequenceconceptindex, section 7.4hott_book
4VM69JJ4Z2statementlem, section 6.3hott_book
transitivity, of inductive coverconceptindex, section B.5hott_book
4W819MXYN1proofproof, section 7.9hott_book
4X0R46C91Jproofproof, section 1.15hott_book
4X7TKKJ1EQdefinitiondefn, section 2.4hott_book
4X8B7SM056definitiondefn, section 2.6hott_book
4XAM6E5MC3statementthm, section 3.8hott_book
algorithmconceptindex, section 5.11hott_book
computation rule, propositionalconceptindex, section 5.2hott_book
4Y0GMA0P4Sproofproof, section 2.9hott_book
4Y6DFTBRC3statementthm, section B.3.2hott_book
effective, equivalence relationconceptindex, section C.1.3hott_book
deductive systemconceptindex, section A.1hott_book
programmingconceptindex, section u1.u7hott_book
classical, analysisconceptindex, section B.5hott_book
type theory, intensionalconceptindex, section A.12.3hott_book
set-quotientconceptindex, section 5.10hott_book
ordered fieldconceptindex, section Bhott_book
50APY9DZ29proofproof, section B.5hott_book
van Kampen with a set of basepointsstatementthm, section 7.7.2hott_book
conjunctionconceptindex, section A.11hott_book
50JCKJJCZWstatementthm, section 4.4hott_book
50TZ6JEPZKstatementthm, section 1.15hott_book
50XRZQJGPBexerciseex, section 8.8hott_book
51N8QSRDA8statementthm, section B.6hott_book
join, of typesconceptindex, section 7.5.3hott_book
free, generation of an inductive typeconceptindex, section 8.1hott_book
truncation, setconceptindex, section 5.9hott_book
logic, truncatedconceptindex, section 9.10hott_book
skeleton, of a CW-complexconceptindex, section 5.6hott_book
equivalenceconceptindex, section 1.4hott_book
54W0KGKQ9Jproofproof, section B.3.2hott_book
geometry, syntheticconceptindex, section 1hott_book
Second proofproofproof, section 1.1hott_book
57NSVZY5CVproofproof, section B.4hott_book
580FCHFWRBexampleeg, section C.3hott_book
58C0BBP602statementcor, section 7.1.4hott_book
natural, transformationconceptindex, section 2.8hott_book
5A6HRKQ7BZproofproof, section C.3hott_book
type, functionconceptindex, section 4.2.4hott_book
5AKH1FJG54statementcor, section 7.1.4hott_book
type, dependent pairconceptindex, section A.6hott_book
5BD2HXBR7Kproofproof, section 2.3hott_book
5BZZSKGK3Dexerciseex, section 7.10hott_book
classifier, subobjectconceptindex, section C.1.4hott_book
set theory, Zermelo--Fraenkelconceptindex, section u1.u5hott_book
natural numbersconceptindex, section 5.10hott_book
5CY5RM1TWEexerciseex, section 8.8hott_book
predecessorconceptindex, section 8.3hott_book
type, colimitconceptindex, section 5.8hott_book
classical, homotopy theoryconceptindex, section 7hott_book
hub and spokeconceptindex, section 5.7hott_book
5EQHPXZRH4statementlem, section 5.10hott_book
idempotent, modalityconceptindex, section 6.7hott_book
5FDRPFJXGPproofproof, section 5.3hott_book
denialconceptindex, section C.4hott_book
constant, primitiveconceptindex, section 4.1hott_book
propositional, equalityconceptindex, section A.1hott_book
Sketch of proofproofproof, section 8.4hott_book
5HX9GHC7RZproofproof, section 7.5.3hott_book
5JS9VVD9EQexampleeg, section 2.1hott_book
truncation, $n$-truncationconceptindex, section 5.9hott_book
5KQ8FVPJKDdefinitiondefn, section 8.4hott_book
Another putative proof of \cref{thm:ordsucc}proofproof, section C.3hott_book
5KZSA7YRRAexerciseex, section 9.11hott_book
assumptionconceptindex, section A.1hott_book
kernel, pairconceptindex, section B.3.2hott_book
localization of inductive coverconceptindex, section B.5hott_book
group, abelianconceptindex, section 5.11hott_book
5MN3SK85NEproofproof, section 5.11hott_book
bounded, quantifierconceptindex, section C.5hott_book
5N5X3BPN8Qexampleeg, section 2.1hott_book
dimension, of pathsconceptindex, section 1hott_book
algorithmconceptindex, section A.1hott_book
preorder, of cardinal numbersconceptindex, section C.2hott_book
5NX2ZTNF65proofproof, section 9.11hott_book
proof, assistant, Coqconceptindex, section 1.15hott_book
function, domain ofconceptindex, section A.2hott_book
Lawvereconceptindex, section u1.u5hott_book
5Q0CY2PF2Mdefinitiondefn, section C.3hott_book
5Q57SR8MV8definitiondefn, section B.5hott_book
5Q765K3PBWdefinitiondefn, section 6.4hott_book
fiberwise, transformationconceptindex, section 3.7hott_book
homotopy, group, of sphereconceptindex, section 7.10hott_book
5QJDZ63E68statementlem, section 9.11hott_book
transport, in dependent function typesconceptindex, section 1.9hott_book
5S9PDK571Nexerciseex, section C.5hott_book
5T7F5610K6statementcor, section 3.6hott_book
5TDFRQF813definitiondefn, section C.3hott_book
path, constantconceptindex, section A.12.1hott_book
real numbers, Cauchyconceptindex, section B.3hott_book
adjoint, functorconceptindex, section 2.5hott_book
judgmental equalityconceptindex, section 5.2hott_book
set-quotientconceptindex, section 5.13hott_book
5X4B81VW10statementcor, section 7.6hott_book
type, emptyconceptindex, section A.7hott_book
completion, Cauchyconceptindex, section B.3hott_book
5XYWFEF71Dproofproof, section 5.11hott_book
impredicative, truncationconceptindex, section 9.11hott_book
flattening lemmaconceptindex, section 7.5.1hott_book
5Z0P3YYNDHdefinitiondefn, section C.5hott_book
sequenceconceptindex, section B.5hott_book
variableconceptindex, section 8.3hott_book
term, convertibility ofconceptindex, section 4.1hott_book
6166QAMEKAexampleeg, section 9.1hott_book
The unstable octahedral axiomexerciseex, section 3.9hott_book
function, surjectiveconceptindex, section C.1.2hott_book
decidable, equalityconceptindex, section B.1hott_book
62HPJFM2W1proofproof, section 6.2hott_book
62JM0294E5exerciseex, section 7.10hott_book
657VF1170Yproofproof, section C.1.2hott_book
65RHCVGRX6proofproof, section 9.8hott_book
Notes on the proof.proofproof, section 7.10hott_book
total, spaceconceptindex, section 7.4hott_book
66VN55FDSNproofproof, section 6.5hott_book
propositional, resizingconceptindex, section Chott_book
671KGGBRJMexerciseex, section 6.7hott_book
674FHF1VSMproofproof, section 5.4hott_book
678TW7XMERstatementlem, section 9.11hott_book
presentation, of a positive type by its constructorsconceptindex, section 1.12hott_book
function, bi-invertibleconceptindex, section 3.3hott_book
type, inductiveconceptindex, section 8.6hott_book
cover, universalconceptindex, section 7.1.3hott_book
69MW334PKRexerciseex, section 7.10hott_book
function, contractibleconceptindex, section 3.4hott_book
loop spaceconceptindex, section 7.1hott_book
interval, arithmeticconceptindex, section B.2.1hott_book
homomorphism, fieldconceptindex, section B.2.3hott_book
6C0KRR81C3definitiondefn, section 7.4hott_book
universal, property, of free groupconceptindex, section 5.11hott_book
latticeconceptindex, section B.2hott_book
natural, isomorphismconceptindex, section 2.2hott_book
bitconceptindex, section 9.3hott_book
6EBVBK07QPexerciseex, section A.12.3hott_book
6EFB258RQXstatementlem, section 5.12hott_book
universe levelconceptindex, section B.2hott_book
identity, functionconceptindex, section 1.4hott_book
6FWT9FQC86proofproof, section B.3.2hott_book
6G41K8B8VQproofproof, section 5.11hott_book
computation rule, for dependent pair typeconceptindex, section A.6hott_book
mathematics, classicalconceptindex, section A.8hott_book
6J0EZHBBTEproofproof, section B.3.2hott_book
$\eta $-expansionconceptindex, section A.5hott_book
6J3XT8DN83proofproof, section 9.11hott_book
Function extensionalitystatementaxiom, section 1.9hott_book
recursion principle, for $\Sn^1$conceptindex, section 5.2hott_book
6KV3ZKYPW9proofproof, section 5.12hott_book
6KVGF79RYEstatementcor, section B.6hott_book
diagramconceptindex, section 1.15hott_book
Cantor's theoremconceptindex, section C.2hott_book
type, identity, as inductiveconceptindex, section 8.8hott_book
recursion principle, for type of booleansconceptindex, section A.8hott_book
6PPYY8HXSVproofproof, section 3.2hott_book
rule, introductionconceptindex, section 4.2.4hott_book
6Q07CH3GNCexerciseex, section 9.11hott_book
6Q7G9A416Eproofproof, section 1.11hott_book
torusconceptindex, section 5.7hott_book
6QREND5HSRexampleeg, section 2.9hott_book
loop spaceconceptindex, section 6.2hott_book
6RMB0M1X1Kproofproof, section 7.1.6hott_book
6RSC6Z1NPEstatementlem, section 2.2hott_book
judgmentconceptindex, section A.1hott_book
initial, fieldconceptindex, section 5.11hott_book
relation, openconceptindex, section B.3.2hott_book
universal, coverconceptindex, section 7.1.2hott_book
6TS25BHRESstatementthm, section 3.2hott_book
relation, effective equivalenceconceptindex, section C.1.3hott_book
horizontal composition, of natural transformationsconceptindex, section 2.2hott_book
6WE53PMA16proofproof, section 6.5hott_book
6WT9KXGYB1statementthm, section 6.7hott_book
6WZM38S400proofproof, section 7.8hott_book
adjoint, equivalence, of types, halfconceptindex, section 3.2hott_book
axiom, of extensionalityconceptindex, section C.3hott_book
computational effectconceptindex, section 6.7hott_book
natural numbers, encoded as $\lst\unit$conceptindex, section 8.2hott_book
6XJ8A4CXKPexerciseex, section 3.9hott_book
6XMHCVBFPRproofproof, section C.1.3hott_book
6XSV9PXQ2Bdefinitiondefn, section 2.4hott_book
6Y852XSQ1Mstatementcor, section C.3hott_book
encode-decode methodconceptindex, section 7.7.1hott_book
6YTR2BQVDPproofproof, section 7.6hott_book
6Z1EX5NYRBdefinitiondefn, section 5.10hott_book
6ZX0CNSKF9statementlem, section 1.3hott_book
7087CF85GYproofproof, section 8.8hott_book
theorem, Feit--Thompsonconceptindex, section u1.u5hott_book
monomorphismconceptindex, section C.1.2hott_book
type theory, extensionalconceptindex, section 1.15hott_book
order, non-strictconceptindex, section B.6hott_book
$(\infty,1)$-toposconceptindex, section 5.12hott_book
71FGBZB0DYdefinitiondefn, section 1.4hott_book
algorithmconceptindex, section u1.u4hott_book
discrete, spaceconceptindex, section u1.u5hott_book
72BTCSQV05exerciseex, section 5.13hott_book
univalence axiom, constructivity ofconceptindex, section u1.u8hott_book
72TX72578Ddefinitiondefn, section B.5hott_book
Encode-decode for Truncations of Loop Spacesstatementlem, section 7.9hott_book
$(\infty,1)$-toposconceptindex, section 6.7hott_book
76HR4JG2MBstatementthm, section 6.1hott_book
group, freeconceptindex, section 5.11hott_book
ex falso quodlibetconceptindex, section A.7hott_book
predecessor, function, truncatedconceptindex, section 5.2hott_book
sequenceconceptindex, section 8.6hott_book
Diaconescustatementthm, section C.1.5hott_book
quantifier, universalconceptindex, section A.11hott_book
Euclid of Alexandriaconceptindex, section 1hott_book
7AD6Y8BW57exerciseex, section 1.15hott_book
power setconceptindex, section 5.10hott_book
type, circleconceptindex, section 5.4hott_book
axiom, Streicher's Axiom K, generalization to $n$-typesconceptindex, section 6.2hott_book
loopconceptindex, section 1hott_book
type theory, informalconceptindex, section A.1hott_book
7BZ5AZBZS8definitiondefn, section 6.6hott_book
7CB9TCCT76proofproof, section 1.13hott_book
7CQP61YP2Xproofproof, section 7.4hott_book
7CWACTY1ZMdefinitiondefn, section 2.2hott_book
7CZ81R3Z3Texerciseex, section 8.8hott_book
univalence axiomconceptindex, section 1.14.1hott_book
computation rule, for function typesconceptindex, section 4.4hott_book
7DX3NK6QG5exerciseex, section 9.11hott_book
7ESGRE42YVdefinitiondefn, section C.1.3hott_book
7F15CDZ41Jstatementlem, section 2.4hott_book
distanceconceptindex, section B.3.1hott_book
homomorphism, fieldconceptindex, section 2.6hott_book
7FKGQVEM58proofproof, section B.2.3hott_book
7GJ0E7JCBKstatementthm, section B.5hott_book
algebraic set theoryconceptindex, section Chott_book
rational numbers, dyadicconceptindex, section B.1hott_book
7J4VVP4W1Astatementthm, section C.1.3hott_book
type, coproductconceptindex, section A.7hott_book
function, linearconceptindex, section 2.7hott_book
strong, collectionconceptindex, section C.5hott_book
logic, predicateconceptindex, section A.11hott_book
uniqueness, principle, propositional, for identities between pairsconceptindex, section 1.6hott_book
Propositional resizingstatementaxiom, section 9.5hott_book
impredicative, encoding of a $\w$-typeconceptindex, section 8.8hott_book
7MBTEVTCVZstatementcor, section 6.7hott_book
mathematics, predicativeconceptindex, section C.1.4hott_book
equivalence, inductionconceptindex, section 8.8hott_book
adjoint, functorconceptindex, section 2.9hott_book
$(\infty,1)$-categoryconceptindex, section 2.9hott_book
loop space, iteratedconceptindex, section 7.4hott_book
decidable, definitional equalityconceptindex, section A.1hott_book
mathematics, formalizedconceptindex, section u1.u6hott_book
7RGQ5AHJFVexerciseex, section 2.9hott_book
2-out-of-3 propertyconceptindex, section 3.7hott_book
7RVRKZPTX3proofproof, section C.1.2hott_book
7RZFN8NWWSstatementthm, section C.1.2hott_book
7TANDWE5C0proofproof, section 6.5hott_book
real numbers, Escard\'o--Simpsonconceptindex, section B.6hott_book
domain, of a constructorconceptindex, section 8.6hott_book
7V2ETATB9Mstatementlem, section 5.9hott_book
7VFZ9TKTRWstatementthm, section 1.13hott_book
group, cyclicconceptindex, section 7hott_book
loop, dependent $n$-conceptindex, section 5.13hott_book
7WPAY4S3K1statementcor, section 3.9hott_book
definition, by structural recursionconceptindex, section 4.1hott_book
functor, covariantconceptindex, section 8.6hott_book
theory, algebraicconceptindex, section 5.11hott_book
``continuity'' of functions in type theoryconceptindex, section 1.2hott_book
7YGP1WSCD6proofproof, section 1.1hott_book
carrierconceptindex, section 1.14hott_book
Flattening lemmastatementlem, section 5.12hott_book
7ZC6C5H7M5proofproof, section 7.5.3hott_book
7ZZX0JW8Y7exerciseex, section 7.10hott_book
805JGRPBY6exerciseex, section 2.9hott_book
universe levelconceptindex, section C.4hott_book
limit, of a Cauchy approximationconceptindex, section B.3.4hott_book
Russell, Bertrandconceptindex, section u1.u1hott_book
81M8N22YM6exerciseex, section A.12.3hott_book
set-quotientconceptindex, section C.1.3hott_book
81RNMQH9A9exerciseex, section C.5hott_book
Grothendieck constructionconceptindex, section 5.12hott_book
828QR1JDE7statementlem, section 7.6hott_book
presentation, of a groupconceptindex, section 5.11hott_book
82RBEY63NYstatementthm, section 8.5hott_book
type, of listsconceptindex, section 8.2hott_book
rule, rewritingconceptindex, section 4.4hott_book
type, productconceptindex, section 1.15hott_book
83GKD0JA9Yproofproof, section 6.5hott_book
classifier, objectconceptindex, section 3.9hott_book
8457HK4TZ4statementcor, section 6.3hott_book
induction principle, for identity type, basedconceptindex, section A.12.1hott_book
orthogonal factorization systemconceptindex, section 6.6hott_book
group, abelianconceptindex, section B.2.1hott_book
84K3QFRHKVexampleeg, section 9.6hott_book
84TW2N3PG5statementlem, section B.3.2hott_book
84W0W96CNEproofproof, section 7.1.5hott_book
856EMYDGF2proofproof, section C.4hott_book
Russell, Bertrandconceptindex, section 9.11hott_book
intensional type theoryconceptindex, section 1.15hott_book
axiom, of choice, type-theoreticconceptindex, section A.6hott_book
type, family ofconceptindex, section 1.3hott_book
homotopy, equivalence, topologicalconceptindex, section u1.u1hott_book
associativity, of path concatenationconceptindex, section 1.1hott_book
universal, property, of suspensionconceptindex, section 5.5hott_book
interval, topological unitconceptindex, section u1.u2hott_book
induction principle, for empty typeconceptindex, section A.7hott_book
First proofproofproof, section 1.1hott_book
886QAFRS0Rexerciseex, section 5.13hott_book
computation rule, propositional, for univalenceconceptindex, section 1.10hott_book
88WGP0TPK0proofproof, section 3.2hott_book
toposconceptindex, section C.5hott_book
adjoint, functor theoremconceptindex, section 5.11hott_book
89VTB22C62statementlem, section 6.6hott_book
89X7PXJNQJexampleeg, section 2.6hott_book
equality, judgmentalconceptindex, section 5.2hott_book
8A4Z6KA4SNstatementlem, section 6.5hott_book
definition, by pattern matchingconceptindex, section 4.4hott_book
axiom, strong collectionconceptindex, section C.5hott_book
8B4RNFTQC7statementthm, section 3.4hott_book
type, of listsconceptindex, section 8.8hott_book
8BW5BZAG2Astatementlem, section 2.9hott_book
path, dependent, in identity typesconceptindex, section 1.11hott_book
8CQ3W0DY9Fproofproof, section 2.2hott_book
path, fibrationconceptindex, section 7.1.2hott_book
paradoxconceptindex, section 9.5hott_book
8EXS3ZABBMproofproof, section C.1.2hott_book
judgmental equalityconceptindex, section 8.1hott_book
8FE32ECACPproofproof, section 7.5.3hott_book
ordinal, plumpconceptindex, section B.6hott_book
8FTWYN53TWstatementlem, section 2.1hott_book
mathematics, classicalconceptindex, section 9.2hott_book
$n$-typeconceptindex, section u1.u7hott_book
$\infty$-groupoidconceptindex, section 1hott_book
computation rule, for $\Sn^1$conceptindex, section 5.2hott_book
integersconceptindex, section 7hott_book
8GQC5W5SHSstatementlem, section B.3.2hott_book
associativity, of function typesconceptindex, section A.2hott_book
8H0DAVGAJKproofproof, section 7.7.2hott_book
loop spaceconceptindex, section 5.5hott_book
category, of typesconceptindex, section 2.9hott_book
excluded middleconceptindex, section C.2hott_book
geometric realizationconceptindex, section 7.7.2hott_book
8K509DXN3Ystatementlem, section 9.5hott_book
Elementary Theory of the Category of Setsconceptindex, section C.5hott_book
recurrenceconceptindex, section A.9hott_book
8PCDXTN0ZPstatementthm, section 3.1hott_book
8PG8NK6RK8statementlem, section C.3hott_book
fibrant replacementconceptindex, section C.1.4hott_book
8PZZS0Q74Bproofproof, section 6.3hott_book
``functoriality'' of functions in type theoryconceptindex, section 9.11hott_book
substitutionconceptindex, section A.1hott_book
finite, lists, type ofconceptindex, section 5.11hott_book
8RT7JZ101Mstatementlem, section B.3.3hott_book
variable, typeconceptindex, section 8.7hott_book
ordered field, admissibleconceptindex, section B.4hott_book
carrierconceptindex, section A.6hott_book
Galois, groupconceptindex, section 2.6hott_book
8T0V235P92proofproof, section 6.1hott_book
8TY9EVVD77exerciseex, section C.5hott_book
type, unitconceptindex, section 1.15hott_book
8V669CKE2Cdefinitiondefn, section 3.2hott_book
discconceptindex, section 5.6hott_book
pointwise, operations on functionsconceptindex, section 1.9hott_book
subtypeconceptindex, section A.11hott_book
``functoriality'' of functions in type theoryconceptindex, section 1.2hott_book
8VKKK6SGSRdefinitiondefn, section B.6hott_book
function extensionalityconceptindex, section 1.5hott_book
8VQRB4AGTVexerciseex, section B.6hott_book
natural numbers, encoded as a $\w$-typeconceptindex, section 8.5hott_book
Eckmann--Hilton argumentconceptindex, section 5.11hott_book
8WSF1TRJJEexerciseex, section 2.9hott_book
mathematics, constructiveconceptindex, section 5.11hott_book
8WWWEPQZQGstatementcor, section 1.4hott_book
apartnessconceptindex, section B.3.3hott_book
First proofproofproof, section 1.3hott_book
8X9QP4ZWC6proofproof, section B.6hott_book
quantifier, existentialconceptindex, section B.2hott_book
8XMQZSW5JRproofproof, section 1.4hott_book
generator, of a groupconceptindex, section 5.11hott_book
8Z389E38CXexampleeg, section 1.4hott_book
8Z6KCNJ4T7statementthm, section 1.15hott_book
theorem, Conway's simplicityconceptindex, section B.6hott_book
transport, in unit typeconceptindex, section 1.8hott_book
$(\infty,1)$-categoryconceptindex, section 2hott_book
supremum, constructor of a $\w$-typeconceptindex, section 8.3hott_book
axiom, of choiceconceptindex, section C.2hott_book
91JWD8X3GBstatementthm, section 7.1.4hott_book
91NXRMNHY7proofproof, section C.1.2hott_book
91W1TCX7FJexampleeg, section 2.1hott_book
natural numbers, isomorphic definition ofconceptindex, section 8.2hott_book
limit, of typesconceptindex, section 1.15hott_book
set theory, Zermelo--Fraenkelconceptindex, section C.5hott_book
fundamental, groupconceptindex, section 7.7.2hott_book
orthogonal factorization systemconceptindex, section C.1.2hott_book
93B5KGDR23exerciseex, section 7.10hott_book
completion, Rezkconceptindex, section 2.9hott_book
codomain, of a functionconceptindex, section A.2hott_book
94CRGY5EF5proofproof, section B.5hott_book
95K3AYR2T5statementthm, section B.3.4hott_book
definition, inductiveconceptindex, section 8hott_book
97NRDJEF29exampleeg, section 7.7.2hott_book
monadconceptindex, section 5.13hott_book
judgmental equalityconceptindex, section 1.5hott_book
99FQY671T9exerciseex, section 1.15hott_book
99H8J1NVATstatementthm, section 8.5hott_book
computation rule, propositionalconceptindex, section 8.5hott_book
topology, pointfreeconceptindex, section B.5hott_book
9AVY4Z0JHKproofproof, section B.5hott_book
9B3YD07574statementcor, section 9.2hott_book
truncation, propositionalconceptindex, section 5.9hott_book
9CHAHKXN63statementcor, section 7.6hott_book
9CPTG7NF7Bexampleeg, section 2.1hott_book
toposconceptindex, section u1.u7hott_book
term, normal form ofconceptindex, section 4.4hott_book
9D09W1RNNDstatementthm, section 9.2hott_book
9D6ZSKM5E6statementlem, section 5.2hott_book
recursion principle, for truncationconceptindex, section 5.9hott_book
together withconceptindex, section A.6hott_book
Bourbakiconceptindex, section 1.15hott_book
9E0PPQ3WH1proofproof, section 1.7hott_book
suspensionconceptindex, section 5.5hott_book
equality, symmetry ofconceptindex, section 1.1hott_book
loop spaceconceptindex, section 7.1.2hott_book
9FHVCXP8B1proofproof, section B.2.3hott_book
9GBQZDDG5Hexerciseex, section 8.8hott_book
9GCJM58YNDproofproof, section 6.2hott_book
mathematics, constructiveconceptindex, section 7hott_book
loop space, iteratedconceptindex, section 1.1hott_book
9HKWGKZ6MRexerciseex, section 9.11hott_book
open, problemconceptindex, section 7.10hott_book
category, well-pointedconceptindex, section C.1.5hott_book
arityconceptindex, section 2.8hott_book
9JZ7FC00J7statementlem, section C.5hott_book
signature, of an algebraic theoryconceptindex, section 5.11hott_book
homotopy-inductive typeconceptindex, section 8.5hott_book
successorconceptindex, section 1.13hott_book
consistency, of arithmeticconceptindex, section C.5hott_book
9KT8G9KQ5Cproofproof, section 1.4hott_book
game, Conwayconceptindex, section B.6hott_book
$\infty$-functorconceptindex, section 1hott_book
9N8XDVR62Wproofproof, section 9.11hott_book
logic, intuitionisticconceptindex, section u1.u7hott_book
transportconceptindex, section 1.7hott_book
9PBQYDYS43proofproof, section 5.10hott_book
9PN4AK5A46statementthm, section 7.2hott_book
recursion principleconceptindex, section 8.1hott_book
target, of a path constructorconceptindex, section 5.6hott_book
Cantorstatementthm, section C.2hott_book
transitivity, of $<$ for surrealsconceptindex, section B.6hott_book
9QN9W8SG4Qproofproof, section B.3.2hott_book
9R1YK55K61statementlem, section 7.1.4hott_book
scopeconceptindex, section A.4hott_book
9RTVMJ73FWexampleeg, section C.3hott_book
propositional, logicconceptindex, section A.11hott_book
analytic mathematicsconceptindex, section 1hott_book
acceptanceconceptindex, section B.6hott_book
recursion principle, for interval typeconceptindex, section 5.3hott_book
intensional type theoryconceptindex, section A.12.3hott_book
9WS1AMP3F8proofproof, section 2.1hott_book
mathematics, formalizedconceptindex, section u1.u5hott_book
9Z0183DSK1statementlem, section C.3hott_book
type, unitconceptindex, section 8.2hott_book
fibrationconceptindex, section 1.7hott_book
A11TYE574Bproofproof, section B.3.3hott_book
higher category theoryconceptindex, section 1hott_book
A182X6BFS0exampleeg, section 2.6hott_book
A18B2N53CJdefinitiondefn, section B.2.1hott_book
A2FDF8Y9BXstatementlem, section 5.12hott_book
A337RA6RFZdefinitiondefn, section C.3hott_book
equality, transitivity ofconceptindex, section 1.1hott_book
plump, ordinalconceptindex, section B.6hott_book
path, 3-conceptindex, section 1.1hott_book
homotopy, groupconceptindex, section 7hott_book
A56RDS08DEdefinitiondefn, section C.2hott_book
A5DREJ7STBdefinitiondefn, section 2.4hott_book
type, unitconceptindex, section 1.8hott_book
A6FC59Z6SHstatementthm, section 6.3hott_book
Homotopy Groupsdefinitiondefn, section 7hott_book
meridianconceptindex, section 5.7hott_book
monomorphismconceptindex, section 2.6hott_book
A6YDB6KHBJstatementcor, section B.6hott_book
mathematics, proof-relevantconceptindex, section A.6hott_book
inverse, in a (pre)categoryconceptindex, section 2.1hott_book
Structure identity principlestatementthm, section 2.8hott_book
A88VF6GZJGstatementlem, section 1.3hott_book
type, universeconceptindex, section 4.2.3hott_book
A8VK1CP9T1statementcor, section 5.10hott_book
$\infty$-groupoid, structure of a typeconceptindex, section 1.1hott_book
vector, spaceconceptindex, section 2.7hott_book
A9D4B5T5BTexerciseex, section 1.15hott_book
bargainingconceptindex, section C.5hott_book
A9PSAPSEVVdefinitiondefn, section C.3hott_book
identity, modalityconceptindex, section 6.7hott_book
non-strict orderconceptindex, section B.3.3hott_book
colimit, of typesconceptindex, section 1.15hott_book
excluded middleconceptindex, section u1.u7hott_book
ABKFC477QBexampleeg, section 7.8hott_book
ABSK9ZAW8Astatementlem, section 6.5hott_book
ABX5F441T1exerciseex, section B.6hott_book
ACDJ73WDX2statementthm, section 7.10hott_book
type, identityconceptindex, section 1.1hott_book
ADTGZPHRG9statementthm, section 3.8hott_book
ADZWFVPB2Fstatementthm, section 8.5hott_book
acceptanceconceptindex, section 2.4hott_book
AEKEZ8SFPKexerciseex, section 3.9hott_book
non-strict orderconceptindex, section B.6hott_book
type, family ofconceptindex, section A.8hott_book
AFMVQ4BDG2exampleeg, section 2.7hott_book
AFZ9KKCSWHstatementlem, section 9.3hott_book
mathematics, formalizedconceptindex, section B.6hott_book
type, mutual inductiveconceptindex, section 8.7hott_book
2-out-of-6 propertyconceptindex, section 3.9hott_book
complete, Segal spaceconceptindex, section 2.9hott_book
AH3X2V59CEproofproof, section 3.8hott_book
AJ0JQ9H78Pexampleeg, section 2.9hott_book
AJHFA3WMY7statementlem, section 6.6hott_book
fibrationconceptindex, section 7.1.2hott_book
AMRGHAFHX0proofproof, section 6.5hott_book
recursion principle, for truncationconceptindex, section 9.7hott_book
denialconceptindex, section 9.4hott_book
path, topologicalconceptindex, section u1.u2hott_book
Segal, spaceconceptindex, section 2.9hott_book
AQVYDXDPMGexampleeg, section 9.1hott_book
ARC01SZJQ1proofproof, section 5.12hott_book
ARV7JA9457statementthm, section 7.1.5hott_book
vector, spaceconceptindex, section B.3.3hott_book
associativity, of addition, of Cauchy realsconceptindex, section B.3.3hott_book
ATMHASTYB2proofproof, section 6.1hott_book
induction principle, for coproductconceptindex, section A.7hott_book
$\infty$-groupoidconceptindex, section 7hott_book
contextconceptindex, section sec:formal-prelimhott_book
interval, open and closedconceptindex, section B.5hott_book
pushoutconceptindex, section 7.5.1hott_book
negative, typeconceptindex, section 1.12hott_book
cone, of a sphereconceptindex, section 5.7hott_book
uniqueness, principle, for identities between functionsconceptindex, section 1.9hott_book
AXMXHFPA2Wstatementlem, section B.3.2hott_book
covariant functorconceptindex, section 8.6hott_book
strict, categoryconceptindex, section 2.9hott_book
AYW1YNW9SDexampleeg, section 5.11hott_book
``functoriality'' of functions in type theoryconceptindex, section 6.2hott_book
type, dependent functionconceptindex, section 1.9hott_book
associativity, of functor composition, coherence ofconceptindex, section 2.2hott_book
pointfree topologyconceptindex, section B.5hott_book
B0JQ9S1TG6definitiondefn, section 3.9hott_book
B10Y16BFE2statementthm, section C.5hott_book
B16NCMC7E1proofproof, section 9.8hott_book
natural numbersconceptindex, section 8.1hott_book
Quillen model categoryconceptindex, section 7hott_book
rational numbers, as Cauchy real numbersconceptindex, section B.3.1hott_book
$\infty$-groupoidconceptindex, section 1.15hott_book
B2KNXMB04Zstatementthm, section 1.11hott_book
theorem, Freudenthal suspensionconceptindex, section 7.6hott_book
successorconceptindex, section 8.1hott_book
retract, of a typeconceptindex, section 6.1hott_book
B4WRJ3BCJ6statementlem, section 5.5hott_book
gaunt categoryconceptindex, section 2.6hott_book
power setconceptindex, section A.8hott_book
universal, propertyconceptindex, section 1.15hott_book
infinitary, algebraic theoryconceptindex, section 5.11hott_book
B70J826FPQstatementlem, section C.3hott_book
B76ABMYG78exerciseex, section 6.7hott_book
B7EXH40BC0proofproof, section 6.3hott_book
B7FKZ1AYC8exampleeg, section 2.4hott_book
B7NBDJZ09Gstatementthm, section C.4hott_book
substitutionconceptindex, section sec:formal-prelimhott_book
category, gauntconceptindex, section 2.6hott_book
heterogeneous equalityconceptindex, section 5.2hott_book
category, cocompleteconceptindex, section C.1.1hott_book
mathematics, classicalconceptindex, section A.11hott_book
univalence axiomconceptindex, section u1.u7hott_book
triangle, inequality for $\RC$conceptindex, section B.3.2hott_book
propositional, resizingconceptindex, section B.5hott_book
BCHQK4TPXKstatementlem, section 6.3hott_book
strong, inductionconceptindex, section C.3hott_book
type, coproductconceptindex, section A.12.3hott_book
value, truthconceptindex, section A.8hott_book
axiom, of reducibilityconceptindex, section 9.11hott_book
BD87PZ6046statementthm, section 5.11hott_book
function, $n$-connectedconceptindex, section 6.5hott_book
BDMGMV5C9Rexerciseex, section B.6hott_book
Freudenthal Equivalencestatementcor, section 7.6hott_book
Eckmann--Hilton argumentconceptindex, section 7hott_book
BE695094XCdefinitiondefn, section 5.8hott_book
stack, completionconceptindex, section 2.9hott_book
BEV5N7QDM9statementlem, section 1.4hott_book
winding, numberconceptindex, section 7.1.4hott_book
BF4ES7QRNSstatementlem, section 1.10hott_book
modal, logicconceptindex, section 6.7hott_book
BF67J8QRVXstatementthm, section C.1.4hott_book
BF9D80XHD6proofproof, section 9.11hott_book
``continuity'' of functions in type theoryconceptindex, section u1.u2hott_book
classical, homotopy theoryconceptindex, section 1hott_book
open, problemconceptindex, section 6.7hott_book
type, universeconceptindex, section 9.1hott_book
BG4NPYG5TQstatementthm, section 6.2hott_book
BHHHHF4J3Kproofproof, section B.2.3hott_book
setconceptindex, section u1.u5hott_book
function, dependentconceptindex, section 1.3hott_book
BK9FPVGKNFstatementlem, section 2.2hott_book
First proofproofproof, section 2.9hott_book
quantifier, universalconceptindex, section 9.7hott_book
Kan complexconceptindex, section 7hott_book
BMM97KBWQ2exerciseex, section A.12.3hott_book
BMN02QS0D3exerciseex, section 9.11hott_book
limit, of a Cauchy approximationconceptindex, section B.2.2hott_book
inverse, approximateconceptindex, section B.1hott_book
automorphism, of $\Z$, successorconceptindex, section 7hott_book
informal type theoryconceptindex, section u1.u6hott_book
functor, adjointconceptindex, section 2.3hott_book
BNQBNG7Q5Hdefinitiondefn, section 7.6hott_book
identityconceptindex, section u1.u3hott_book
theorem, van Kampenconceptindex, section 7.7hott_book
axiomatic freedomconceptindex, section A.11hott_book
BQ7BM4JYNZstatementlem, section C.3hott_book
BQD023FC08exerciseex, section 1.15hott_book
unit, intervalconceptindex, section u1.u2hott_book
transitivity, of $\leq$ for surrealsconceptindex, section B.6hott_book
axiom, of infinityconceptindex, section C.5hott_book
paradoxconceptindex, section 8.6hott_book
category, skeletalconceptindex, section 2.1hott_book
BTDT3FSBVJexerciseex, section 3.9hott_book
BTEJZ6YA1Mstatementthm, section C.1.3hott_book
type, of listsconceptindex, section 8.7hott_book
path, topologicalconceptindex, section 1hott_book
proof, assistantconceptindex, section 5.13hott_book
algebraic set theoryconceptindex, section C.5hott_book
variableconceptindex, section A.10hott_book
red herring principleconceptindex, section 2.6hott_book
BWW6AJ87N7proofproof, section 1.3hott_book
uniqueness, principle, for function typesconceptindex, section A.12.3hott_book
simplicial, setsconceptindex, section 7hott_book
BZKA1HHEA2statementlem, section C.3hott_book
BZX8688E6Adefinitiondefn, section 6.7hott_book
consistencyconceptindex, section u1.u7hott_book
type, inductive-recursiveconceptindex, section 8.7hott_book
C1J9JRYV5Texampleeg, section 9.1hott_book
C2T8WSXSTEstatementlem, section 7.5.2hott_book
skeleton, of a CW-complexconceptindex, section 7.7.2hott_book
natural numbersconceptindex, section A.9hott_book
real numbers, Cauchyconceptindex, section B.4hott_book
``functoriality'' of functions in type theoryconceptindex, section 9.1hott_book
isomorphism, naturalconceptindex, section 2.2hott_book
C4PVH8HH6Hdefinitiondefn, section 9.11hott_book
Fregeconceptindex, section 8.8hott_book
C5QVHKSZ57statementlem, section 7.5.1hott_book
unique, factorization systemconceptindex, section 6.6hott_book
axiom, of separationconceptindex, section C.5hott_book
simplicial, setsconceptindex, section 2.9hott_book
type, $n$-sphereconceptindex, section 5.5hott_book
type, universeconceptindex, section A.3hott_book
loop spaceconceptindex, section 1.1hott_book
C8TEJTKXKKexerciseex, section 5.13hott_book
CA7XKM7R66proofproof, section 3.2hott_book
CABCFCDK8Nproofproof, section 9.11hott_book
fibrant replacementconceptindex, section 2.9hott_book
CBP44JW1Q9proofproof, section 7.3hott_book
CCVH9AYJ5Zexerciseex, section 9.11hott_book
Second proofproofproof, section 2.9hott_book
CE5GS7625Estatementlem, section 2.4hott_book
ordered fieldconceptindex, section B.3.4hott_book
path, dependent, in function typesconceptindex, section 1.9hott_book
CG26DWGYJMproofproof, section 2.1hott_book
Feit--Thompson theoremconceptindex, section u1.u5hott_book
CG2YNBVF5Gproofproof, section C.2hott_book
infix notationconceptindex, section 4.1hott_book
Universal Cover of $\Sn^1$definitiondefn, section 7.1.3hott_book
CGYCFHMKMVproofproof, section B.3.2hott_book
analysis, classicalconceptindex, section B.5hott_book
finite, sets, family ofconceptindex, section A.12.3hott_book
Kan complexconceptindex, section 4.4hott_book
type, universe, Russell-styleconceptindex, section A.12.3hott_book
univalence axiomconceptindex, section 1.5hott_book
CJ8SFZMSM5statementthm, section B.6hott_book
CJAARCA42Zexerciseex, section C.5hott_book
CJEPZEM1HAproofproof, section 2.7hott_book
cofiberconceptindex, section 7.7.2hott_book
torusconceptindex, section 7.7.2hott_book
transitivity, of $<$ in a fieldconceptindex, section B.2.1hott_book
resizingconceptindex, section C.1.3hott_book
CME6AMW4VPstatementthm, section 2.9hott_book
CMQRE960ZXexerciseex, section 6.7hott_book
comonadconceptindex, section 6.7hott_book
canonicityconceptindex, section u1.u8hott_book
CND0NSAT23definitiondefn, section B.3.2hott_book
orthogonal factorization systemconceptindex, section 6.7hott_book
proof, assistantconceptindex, section 7hott_book
pullbackconceptindex, section 3.8hott_book
programmingconceptindex, section 8.2hott_book
real numbers, Dedekindconceptindex, section B.2hott_book
type, family of, inductiveconceptindex, section 8.7hott_book
application, of hypothesis or theoremconceptindex, section A.11hott_book
CQD0V914BVproofproof, section C.1.5hott_book
proposition, as typesconceptindex, section 9.2hott_book
power setconceptindex, section B.5hott_book
function, dependentconceptindex, section A.4hott_book
contextconceptindex, section 4.2.1hott_book
CS52JYBXQYstatementlem, section 5.3hott_book
CSQ0T48NW9definitiondefn, section 5.11hott_book
CSVPQK3ECMproofproof, section 2.2hott_book
CSWR9B3Z3Pstatementlem, section 4.4hott_book
CVKETF90D8statementlem, section 1.3hott_book
CVKKWQB227statementcor, section 5.4hott_book
CVNRQH2ZZ8statementlem, section 5.10hott_book
algorithmconceptindex, section u1.u6hott_book
graphconceptindex, section 1.15hott_book
function extensionalityconceptindex, section 4.3.1hott_book
retractionconceptindex, section 3.6hott_book
univalence axiomconceptindex, section 7hott_book
truncation, propositionalconceptindex, section 9.7hott_book
function, injectiveconceptindex, section C.1.2hott_book
associativity, of list concatenationconceptindex, section 5.11hott_book
type, 2-sphereconceptindex, section 5.1hott_book
defining equationconceptindex, section 4.1hott_book
D0PATNC9G3exampleeg, section 9.6hott_book
D0WN2SS47Pexerciseex, section 6.7hott_book
mathematics, classicalconceptindex, section 9.6hott_book
D15SPAMGN7statementthm, section 6.3hott_book
type theory, formalconceptindex, section 4hott_book
vector, induction principle forconceptindex, section 8.7hott_book
D1S3CSMFZ7proofproof, section 5.4hott_book
variableconceptindex, section 4.2.1hott_book
universal, property, of $\w$-typeconceptindex, section 8.4hott_book
group, abelianconceptindex, section 7.3hott_book
type, singletonconceptindex, section A.12.1hott_book
power setconceptindex, section C.3hott_book
homomorphism, semigroupconceptindex, section 1.14.2hott_book
homotopy, hypothesisconceptindex, section 1hott_book
D4J7HVQEMJstatementthm, section B.3.3hott_book
type theory, informalconceptindex, section u1.u6hott_book
coherenceconceptindex, section 3.2hott_book
initial, $\sigma$-frameconceptindex, section B.2hott_book
D4V6PYT86Hstatementthm, section 5.11hott_book
D4VDDCQ09Qexerciseex, section B.6hott_book
Univalencestatementaxiom, section 1.10hott_book
type, unitconceptindex, section 9.11hott_book
D6AQVDHPPBstatementthm, section 8.4hott_book
proposition, as typesconceptindex, section A.11hott_book
proof, assistantconceptindex, section A.12.3hott_book
$(\infty,1)$-categoryconceptindex, section 6.3hott_book
theorem, Conway's 0conceptindex, section B.6hott_book
D8B2WVF1VWexerciseex, section B.6hott_book
modalityconceptindex, section 6.7hott_book
recursion principle, for a modalityconceptindex, section 6.7hott_book
logic, propositionalconceptindex, section A.11hott_book
D8RN8WNV7Rstatementlem, section C.3hott_book
equation, definingconceptindex, section 4.1hott_book
associativity, of $\Sigma$-typesconceptindex, section 1.15hott_book
DB8E83NRBHproofproof, section B.2.1hott_book
DBN2CH6YRAproofproof, section 2.1hott_book
DBT8N1HA21exerciseex, section 3.9hott_book
DC7A6FKMXHproofproof, section 1.8hott_book
DCAZ4BQ4ADstatementthm, section 1.7hott_book
pentagon, Mac Laneconceptindex, section 1hott_book
excluded middleconceptindex, section B.2hott_book
distanceconceptindex, section B.3.3hott_book
Cauchy, sequenceconceptindex, section B.3.1hott_book
DG21SCPRXJstatementlem, section 5.4hott_book
limited principle of omniscienceconceptindex, section C.5hott_book
function extensionalityconceptindex, section A.12.3hott_book
toposconceptindex, section 2.9hott_book
DHES6JR3K7statementthm, section 1.12hott_book
induction principle, for identity typeconceptindex, section 1hott_book
DHZSD2EHMBstatementlem, section 2.9hott_book
Proof of \cref{thm:hlevel-loops}proofproof, section 6.2hott_book
DJXYC7H8WRstatementthm, section 2.5hott_book
DK17NXZ3QHstatementcor, section 7.3hott_book
monotonicity, of inductive coverconceptindex, section B.5hott_book
DMEBN2BP66exerciseex, section 8.8hott_book
computation rule, for product typesconceptindex, section A.5hott_book
DN835ZYBK6exerciseex, section 9.11hott_book
adjoint, linear mapconceptindex, section 2.7hott_book
DNCMPX6XFMexerciseex, section 1.15hott_book
univalence axiomconceptindex, section 9.2hott_book
resizingconceptindex, section C.5hott_book
DPQ2HPNPH2proofproof, section B.3.3hott_book
induction principle, for an inductive typeconceptindex, section 8.6hott_book
``continuity'' of functions in type theoryconceptindex, section 1.3hott_book
pullbackconceptindex, section 5.8hott_book
natural numbers, encoded as a $\w$-typeconceptindex, section 8.3hott_book
elaboration, in type theoryconceptindex, section 4.2.11hott_book
DT5GE91S3Cstatementcor, section C.4hott_book
DT7WJMHYSNstatementlem, section 2.2hott_book
DTCFB5M36Jstatementlem, section C.1.2hott_book
relation, reflexiveconceptindex, section 6.2hott_book
variableconceptindex, section sec:formal-prelimhott_book
Kan complexconceptindex, section u1.u7hott_book
colimit, of typesconceptindex, section 6.7hott_book
algebra, colimits ofconceptindex, section 5.11hott_book
equivalence, as contractible functionconceptindex, section 3.4hott_book
toposconceptindex, section 9.11hott_book
DX7VCKHRXZstatementlem, section C.1.2hott_book
basepointconceptindex, section 6.5hott_book
finite, sets, family ofconceptindex, section A.3hott_book
target, of a path constructorconceptindex, section 5.13hott_book
loop, $n$-conceptindex, section 7hott_book
DY9DMSBXHHexampleeg, section B.6hott_book
DY9GHJMFYWproofproof, section B.3.3hott_book
inductive, predicateconceptindex, section 8.7hott_book
DYNXAZW7CNproofproof, section B.3.2hott_book
First proofproofproof, section 1.3hott_book
Contractible mapsdefinitiondefn, section 3.4hott_book
DZD5C763HQstatementthm, section 3.4hott_book
``continuity'' of functions in type theoryconceptindex, section 1.4hott_book
E09SM7EZ1Cproofproof, section 2.4hott_book
axiom, of choiceconceptindex, section 2.9hott_book
E0E1RXBF92statementcor, section B.2.3hott_book
E193KJTWZ5proofproof, section 3.9hott_book
loop spaceconceptindex, section 7.4hott_book
retractionconceptindex, section 6.1hott_book
adjoint, functorconceptindex, section 1hott_book
homotopy, (pre)category of typesconceptindex, section 2.1hott_book
Cauchy, sequenceconceptindex, section B.3hott_book
structure, semigroupconceptindex, section 1.14hott_book
E38G25JFF6statementcor, section 4.4hott_book
E3QESTN76Sexampleeg, section 5.13hott_book
E5RACS7F3Gexerciseex, section B.6hott_book
type, positiveconceptindex, section 1.12hott_book
E60RKHBS6Kproofproof, section 5.12hott_book
E6J07WWXT4proofproof, section 5.10hott_book
E6QBGXBPNFproofproof, section 7.4hott_book
associativity, of addition, of natural numbersconceptindex, section A.9hott_book
Archimedean principle for $\RC$statementthm, section B.3.3hott_book
topology, Lawvere-Tierneyconceptindex, section 6.7hott_book
isomorphism, invariance underconceptindex, section 2.9hott_book
E94E7N55BXproofproof, section C.2hott_book
finite, -dimensional vector spaceconceptindex, section 2.7hott_book
E9PR3DKD2Bexerciseex, section 9.11hott_book
axiom, of choice, countableconceptindex, section B.6hott_book
universal, property, of identity typeconceptindex, section 1.15hott_book
EA7VXJQYDXproofproof, section 1.6hott_book
EAHK5AYWQ8proofproof, section B.6hott_book
completion, of a metric spaceconceptindex, section B.6hott_book
integersconceptindex, section 7.1.3hott_book
EB9QR6DWPPexampleeg, section 9.1hott_book
EBC0ED55K2exerciseex, section C.5hott_book
EC5TCK5PJ4proofproof, section 6.6hott_book
homotopy, equivalence, topologicalconceptindex, section 7hott_book
strict, categoryconceptindex, section 2hott_book
EEAPQ9N9X5exerciseex, section 8.8hott_book
type, universeconceptindex, section 4.1.1hott_book
Transportstatementlem, section 1.3hott_book
EGEG2F52K2statementlem, section 6.4hott_book
proof, assistant, \NuPRLconceptindex, section 9.11hott_book
rule, versus axiomsconceptindex, section A.1hott_book
canonicityconceptindex, section A.1hott_book
propositional, resizingconceptindex, section B.6hott_book
localeconceptindex, section B.5hott_book
EK5Y8T9X2Cproofproof, section 2.8hott_book
mathematics, classicalconceptindex, section B.5hott_book
predicate, logicconceptindex, section A.11hott_book
EKNTCS29M5exerciseex, section 1.15hott_book
EKVWMK45GMproofproof, section 6.1hott_book
EMHHM8VWWZproofproof, section 1.2hott_book
EN6DM7JE1Hexerciseex, section 6.7hott_book
ENZ05JVGCNstatementcor, section 2.5hott_book
EQK2KF3E2Pproofproof, section 2.5hott_book
EQYRA3W34Xstatementlem, section 5.12hott_book
transport, in identity typesconceptindex, section 1.11hott_book
ERCHX0TGPPproofproof, section 7.6hott_book
type, productconceptindex, section 4.2.5hott_book
decidable, equalityconceptindex, section 6.2hott_book
``naturality'' of homotopiesconceptindex, section 1.4hott_book
ETSZZ0DVKXstatementlem, section B.3.3hott_book
ETT9EV5ZM3definitiondefn, section 8.8hott_book
mathematics, classicalconceptindex, section 9.8hott_book
set theory, algebraicconceptindex, section Chott_book
EVQ90JHJNZstatementlem, section 3.2hott_book
EW1CJTMPC4exerciseex, section 2.9hott_book
EW24WDKCCFstatementcor, section B.2.2hott_book
$n$-typeconceptindex, section 6hott_book
EWWHZPBC5Xproofproof, section 3.6hott_book
Eckmann--Hiltonstatementthm, section 1.1hott_book
EXMYDFH5AVproofproof, section C.3hott_book
EZ3A1XP3H3definitiondefn, section 2.7hott_book
power setconceptindex, section C.5hott_book
type, circleconceptindex, section 5.1hott_book
theorem, Hedberg'sconceptindex, section 6.2hott_book
Tierneyconceptindex, section 6.7hott_book
F000AF45KBproofproof, section 5.4hott_book
polarityconceptindex, section 1.12hott_book
F0VVY9AK5Sproofproof, section 5.9hott_book
F154D5W3WZstatementthm, section C.5hott_book
F1X8VEPGKNproofproof, section 9.5hott_book
recursion principle, for suspensionconceptindex, section 5.5hott_book
F261B714XNdefinitiondefn, section 2.1hott_book
type, productconceptindex, section A.5hott_book
equivalence, half adjointconceptindex, section 3.2hott_book
F445N8HVF2statementthm, section 2.9hott_book
paradoxconceptindex, section A.3hott_book
plump, successorconceptindex, section C.5hott_book
loop space, iteratedconceptindex, section 5.11hott_book
F8CQ3968PVexerciseex, section 6.7hott_book
theorem, four-colorconceptindex, section u1.u6hott_book
Proof of \cref{thm:freudenthal}proofproof, section 7.6hott_book
F9H743N9P3proofproof, section C.5hott_book
FA1K2CJKT6proofproof, section 7.7.1hott_book
FAB3PY2QA5statementlem, section 1.2hott_book
FAH96N5SNXexerciseex, section 1.15hott_book
FARTHY9W1Wproofproof, section 3.4hott_book
FAXHZTJMJNstatementlem, section 2.1hott_book
type, of listsconceptindex, section 8.1hott_book
pair, unorderedconceptindex, section C.5hott_book
Diaconescu's theoremconceptindex, section C.1.5hott_book
$\infty$-groupconceptindex, section 5.11hott_book
FCHDNMSB17statementlem, section 6.2hott_book
normalizationconceptindex, section 4.4hott_book
First proofproofproof, section 1.3hott_book
adjoining a disjoint basepointconceptindex, section 5.5hott_book
Second proofproofproof, section 1.3hott_book
FDT33QAASFexerciseex, section C.5hott_book
Yoneda, lemmaconceptindex, section 2.5hott_book
FE5VJF2P9Fproofproof, section 7.4hott_book
FEV0FVRF4Wexerciseex, section A.12.3hott_book
FEXN1FCBJBstatementlem, section 5.2hott_book
rules of type theoryconceptindex, section 4hott_book
cut, Dedekindconceptindex, section B.6hott_book
encode-decode methodconceptindex, section 2.9hott_book
recursion principle, for an inductive typeconceptindex, section 8.6hott_book
metric spaceconceptindex, section B.5hott_book
van Kampen theoremconceptindex, section 7.7hott_book
type, colimitconceptindex, section 1.15hott_book
$\infty$-groupoidconceptindex, section 5.1hott_book
cover, universalconceptindex, section 7.1.2hott_book
variableconceptindex, section 4.1hott_book
positive, typeconceptindex, section 1.12hott_book
typical ambiguityconceptindex, section 4.2.11hott_book
monoid, freeconceptindex, section 5.13hott_book
FMK2ZS9958proofproof, section 5.10hott_book
FMV6ANVTV0statementlem, section 5.12hott_book
FNCAXNFXRFproofproof, section B.3.2hott_book
category, completeconceptindex, section C.1.1hott_book
FP7R5PEMKFexerciseex, section 9.11hott_book
logic, of mere propositionsconceptindex, section 9.3hott_book
choice operatorconceptindex, section 9.2hott_book
FRSGVWKJ3Ndefinitiondefn, section 2.1hott_book
extensional, type theoryconceptindex, section 1.15hott_book
classical, category theoryconceptindex, section 2.7hott_book
FT8H1MGA06definitiondefn, section 1.1hott_book
FV91SMJ3VEexerciseex, section 1.15hott_book
type, emptyconceptindex, section 1.15hott_book
rounded, relationconceptindex, section B.3.2hott_book
mathematics, classicalconceptindex, section 1.15hott_book
FWSBF5CM4Hexerciseex, section 6.7hott_book
loop space, iteratedconceptindex, section 5.4hott_book
reflective, subcategoryconceptindex, section 6.3hott_book
classical, analysisconceptindex, section Bhott_book
mathematics, constructiveconceptindex, section A.9hott_book
$(\infty,1)$-toposconceptindex, section 7hott_book
propositional, resizingconceptindex, section B.2hott_book
G18T7MAPRQproofproof, section 6.5hott_book
G1JXKTNM8Cproofproof, section C.3hott_book
G1S72PRJAKstatementlem, section C.1.5hott_book
equivalence, as bi-invertible functionconceptindex, section 3.3hott_book
G29V2JXQWFstatementthm, section 4.4hott_book
type, identityconceptindex, section 1.11hott_book
foundationsconceptindex, section u1hott_book
fiberwise, transformationconceptindex, section 6.5hott_book
G4FC52F76Mstatementlem, section 3.1hott_book
type, unitconceptindex, section 4.2.8hott_book
induction principle, for $\w$-typesconceptindex, section 8.3hott_book
G5957ZG4YMdefinitiondefn, section B.5hott_book
mathematics, classicalconceptindex, section 2.7hott_book
G5V8E5GECKproofproof, section 5.3hott_book
colimit, of typesconceptindex, section 5.8hott_book
G6YA8H478Jproofproof, section B.3.3hott_book
propositional resizingconceptindex, section C.1.3hott_book
G70EQK0AJSdefinitiondefn, section 7.5.2hott_book
cell complexconceptindex, section 5.6hott_book
angerconceptindex, section 9.2hott_book
G84KF6D4FWdefinitiondefn, section B.3.1hott_book
G882WDSV65exerciseex, section A.12.3hott_book
G8AZPY7P93statementcor, section 3.4hott_book
topological, spaceconceptindex, section u1.u2hott_book
addition, of ordinal numbersconceptindex, section C.5hott_book
Lawvereconceptindex, section 6.7hott_book
universal, property, of truncationconceptindex, section 6.3hott_book
impredicative, quotientconceptindex, section C.1.3hott_book
mathematics, predicativeconceptindex, section B.5hott_book
CW complexconceptindex, section u1.u4hott_book
GAG5QJX1CTproofproof, section 7.5.1hott_book
mathematics, constructiveconceptindex, section C.1.4hott_book
GASG49MNAFproofproof, section B.2.1hott_book
adjoint, equivalenceconceptindex, section 2.9hott_book
type, inductive-inductiveconceptindex, section 8.7hott_book
ordinal, trichotomy ofconceptindex, section C.4hott_book
total, recursive definitionconceptindex, section 4.1hott_book
$(\infty,1)$-toposconceptindex, section 7.8hott_book
GDHS0PHXACstatementlem, section 5.3hott_book
cohomologyconceptindex, section 7hott_book
GEFRT8FMH9statementthm, section 6.4hott_book
reduction, of a word in a free groupconceptindex, section 5.11hott_book
geometric realizationconceptindex, section 7hott_book
quantifier, existentialconceptindex, section 9.6hott_book
Eckmann--Hilton argumentconceptindex, section 7.4hott_book
GHW0CHF0SVdefinitiondefn, section 7.1.4hott_book
recursion principle, for empty typeconceptindex, section A.7hott_book
equality, definitionalconceptindex, section 5.2hott_book
reflection ruleconceptindex, section 1.15hott_book
logic, constructive vs classicalconceptindex, section 9.4hott_book
GNF6RJ6Q5Pproofproof, section 6.7hott_book
type, identityconceptindex, section 1.15hott_book
rule, formationconceptindex, section A.5hott_book
GPBTRMT8KGexerciseex, section 7.10hott_book
mere propositionconceptindex, section 9.5hott_book
``continuity'' of functions in type theoryconceptindex, section 6.2hott_book
variable, boundconceptindex, section 4.2.5hott_book
mathematics, proof-relevantconceptindex, section A.11hott_book
source, of a path constructorconceptindex, section 5.13hott_book
GSGZ9S56CKexerciseex, section 6.7hott_book
object, classifierconceptindex, section 3.9hott_book
generation, of an $\infty$-groupoidconceptindex, section 5.1hott_book
winding, mapconceptindex, section 7.1.2hott_book
trichotomy of ordinalsconceptindex, section C.4hott_book
type theory, formalconceptindex, section u1.u6hott_book
small, typeconceptindex, section u1.u3hott_book
stability, and descentconceptindex, section 5.12hott_book
transportconceptindex, section 1.10hott_book
free, product, amalgamatedconceptindex, section 7.7.2hott_book
$\infty$-groupoidconceptindex, section 8.8hott_book
path, dependent, in dependent function typesconceptindex, section 1.9hott_book
colimit, of setsconceptindex, section 5.9hott_book
GZ4PE21WH3proofproof, section 3.8hott_book
based mapconceptindex, section 5.5hott_book
H00GKHGXYTstatementlem, section 5.10hott_book
H02VS5MFCPproofproof, section 7.1.4hott_book
automorphism, of extensional well-founded relationsconceptindex, section C.3hott_book
H09CG92338exerciseex, section 9.11hott_book
ordinal, plumpconceptindex, section C.5hott_book
First proofproofproof, section 1.3hott_book
H0WJV4D1KNproofproof, section B.3.4hott_book
H1N1PB8VRWexampleeg, section C.3hott_book
torus, induction principle forconceptindex, section 5.6hott_book
H299FF08RTstatementlem, section 5.11hott_book
consistencyconceptindex, section 8.6hott_book
#1conceptindex, section 9.u2hott_book
ordered field, archimedeanconceptindex, section B.6hott_book
set theory, algebraicconceptindex, section C.5hott_book
representable functorconceptindex, section 2.5hott_book
sequence, exactconceptindex, section 7.8hott_book
reflexivity, of a relationconceptindex, section 6.2hott_book
vectorconceptindex, section 8.7hott_book
Stability for Spheresstatementcor, section 7.6hott_book
H5619ZXMCKexerciseex, section 8.8hott_book
H6ADY478E3exerciseex, section 5.13hott_book
H6EJNNZSR0definitiondefn, section 6.4hott_book
axiom, of choice, countableconceptindex, section Bhott_book
excluded middleconceptindex, section C.1.5hott_book
function extensionalityconceptindex, section 9.11hott_book
H7GF0NDD34definitiondefn, section 7.1.4hott_book
``functoriality'' of functions in type theoryconceptindex, section 1.9hott_book
mathematics, formalizedconceptindex, section 8.7hott_book
Lawvereconceptindex, section Chott_book
typical ambiguityconceptindex, section 4.1.1hott_book
$\infty$-groupoidconceptindex, section 7.8hott_book
covering spaceconceptindex, section 7.10hott_book
odd-order theoremconceptindex, section u1.u5hott_book
HBR3DKHWZKexerciseex, section 5.13hott_book
function, codomain ofconceptindex, section A.2hott_book
HC90G3A4F5statementlem, section 3.2hott_book
partial orderconceptindex, section B.2.1hott_book
HCX0JPZDTTproofproof, section 2.4hott_book
denseconceptindex, section B.2.1hott_book
HDW5QMGT5Astatementthm, section 7.8hott_book
functional relationconceptindex, section A.2hott_book
$\lambda$-abstractionconceptindex, section A.10hott_book
HFJBHZ26BWstatementthm, section 3.7hott_book
HFM7XDRAYYdefinitiondefn, section B.2.2hott_book
kernel, pairconceptindex, section C.1.3hott_book
HFVV7CMMF7statementthm, section 7.4hott_book
setoidconceptindex, section 5.13hott_book
HGEMT19GDBproofproof, section 5.4hott_book
denialconceptindex, section C.1.5hott_book
Conway's Theorem 0statementthm, section B.6hott_book
HHHYHGGVMKexerciseex, section 7.10hott_book
HJJQW1SH3Bstatementlem, section 5.10hott_book
HK0F5G3E45proofproof, section 6.6hott_book
HKEQRQ3CZYproofproof, section 7.1.5hott_book
HKQ5VHPPPYproofproof, section 2.1hott_book
HKXY2B3C3Astatementcor, section 4.4hott_book
HMCY2Z0618statementlem, section 7.3hott_book
HMKD1B2PBRstatementthm, section 7.5.3hott_book
HMRHA0G7QWstatementthm, section B.3.3hott_book
HMS5088XE0statementlem, section 1.1hott_book
axiom, of set theory, for the cumulative hierarchyconceptindex, section C.5hott_book
HPC5CXJPKKexerciseex, section B.6hott_book
encode-decode methodconceptindex, section 1.13hott_book
HQ588V8TE3statementlem, section 2.5hott_book
HQAWZ4SA1Mproofproof, section 6.3hott_book
Hedberg's theoremconceptindex, section 6.2hott_book
HRS0Q5KGWEproofproof, section 8.4hott_book
Hedberg's theoremconceptindex, section 9.11hott_book
HSJ8A9RQAYstatementthm, section C.3hott_book
induction principle, for truncationconceptindex, section 9.11hott_book
AUTOMATHconceptindex, section 4.4hott_book
HT69C08ZVGstatementlem, section 3.1hott_book
universal, property, of cartesian productconceptindex, section 1.15hott_book
HTDSJYBKDAproofproof, section 7.8hott_book
relation, irreflexiveconceptindex, section B.2.1hott_book
HTNS029HV3statementthm, section 6.1hott_book
HTWGTFFDZCstatementlem, section 6.5hott_book
loop space, iteratedconceptindex, section 6.2hott_book
HWPN2A0VXVdefinitiondefn, section 6.4hott_book
HX2Z8WKW2Astatementlem, section 8.5hott_book
uniqueness, principleconceptindex, section 4.2.4hott_book
Postnikov towerconceptindex, section u1.u7hott_book
HYKNTHVG1Mexampleeg, section 2.7hott_book
computation rule, for function typesconceptindex, section 4.1hott_book
HZKEXJZ0B7statementlem, section 1.3hott_book
recurrenceconceptindex, section 8.8hott_book
J1TNTY7S94proofproof, section B.3.2hott_book
Freudenthal suspension theoremconceptindex, section 7.6hott_book
axiom, Whitehead's principleconceptindex, section 7.8hott_book
induction principle, for $\Sn^1$conceptindex, section 5.4hott_book
J4QGPMPKV0proofproof, section 1.15hott_book
J4XV9E1ZNNstatementcor, section C.4hott_book
J5MSAZ7W5Dexerciseex, section A.12.3hott_book
natural numbersconceptindex, section 1.13hott_book
J675476AHTproofproof, section B.2.1hott_book
J68QY8NJ1Aexerciseex, section 2.9hott_book
J6D4K866T1statementlem, section 9.3hott_book
ordered field, archimedeanconceptindex, section B.2.1hott_book
uniqueness, principle, propositional, for dependent pair typesconceptindex, section 1.7hott_book
acceptanceconceptindex, section 5.11hott_book
J8KKAPT9Q2exerciseex, section B.6hott_book
identity, systemconceptindex, section 8.8hott_book
classical, category theoryconceptindex, section 2.9hott_book
reflexivity, of inductive coverconceptindex, section B.5hott_book
JA6XA1GMZZproofproof, section 3.3hott_book
JAY0KRKQ2Kstatementlem, section C.4hott_book
JB3GDCB7B1proofproof, section 6.6hott_book
JB43TGDH3Fexampleeg, section 7.7.2hott_book
JBQ291VKRHstatementcor, section 2.5hott_book
function, bi-invertibleconceptindex, section 3hott_book
JCMT3H2JGYexerciseex, section 7.10hott_book
JCN5T1J103proofproof, section 5.2hott_book
equivalenceconceptindex, section 1.10hott_book
equality, heterogeneousconceptindex, section 5.2hott_book
JD3F2GG1AFstatementthm, section 8.1hott_book
JDBMNFM9R7exerciseex, section B.6hott_book
JDK0Q2CS9Kexerciseex, section 6.7hott_book
relation, bitotalconceptindex, section C.5hott_book
category, locally cartesian closedconceptindex, section C.1.4hott_book
Eckmann--Hilton argumentconceptindex, section 1.1hott_book
uniqueness, principle, for product typesconceptindex, section A.12.3hott_book
JEPAKWS8JKstatementthm, section C.3hott_book
JF8XFW3VAGstatementlem, section 1.10hott_book
JFESH8NTDDdefinitiondefn, section C.5hott_book
topological, spaceconceptindex, section u1.u1hott_book
JG7YF4P0HDproofproof, section 6.2hott_book
homotopy, group, of sphereconceptindex, section 7.6hott_book
JGQ9M3TP5Jexerciseex, section A.12.3hott_book
topological, pathconceptindex, section u1.u2hott_book
homotopyconceptindex, section 1.9hott_book
JHHHZCRGVKproofproof, section 1.4hott_book
lax colimitconceptindex, section 5.12hott_book
JK5PMZ4GVHdefinitiondefn, section 8.4hott_book
JKGTCYZVHTproofproof, section 7.2hott_book
JPZJGRR224proofproof, section C.3hott_book
JQQRNNK2JFexerciseex, section 9.11hott_book
JQXX5TFZPYproofproof, section 3.4hott_book
parameter, spaceconceptindex, section A.1hott_book
excluded middleconceptindex, section C.3hott_book
recursion principle, for coproductconceptindex, section A.7hott_book
JSEXHHJC6Rdefinitiondefn, section 7.4hott_book
compactness, Heine--Borelconceptindex, section B.5hott_book
proof, by contradictionconceptindex, section 9.4hott_book
Lawvereconceptindex, section A.12.3hott_book
JT9N9RFMNKstatementthm, section 3.9hott_book
JTT2YPPGNFproofproof, section 7.1.4hott_book
Dependent mapstatementlem, section 1.3hott_book
stability, of homotopy groups of spheresconceptindex, section 7.6hott_book
encode-decode methodconceptindex, section 1.12hott_book
small, setconceptindex, section 2.1hott_book
van Kampen theoremconceptindex, section 2.9hott_book
induction principle, for Cauchy realsconceptindex, section B.3.2hott_book
JXAJR1NRMTproofproof, section C.1.5hott_book
JXMZ34CA42exerciseex, section 7.10hott_book
JXWXFQENQKstatementlem, section 2.1hott_book
limit, of setsconceptindex, section C.1.1hott_book
uniqueness, of identity proofsconceptindex, section A.12.3hott_book
JYV1APHX3Ndefinitiondefn, section C.2hott_book
JZ9N84G2PHexampleeg, section 9.1hott_book
type, unitconceptindex, section A.5hott_book
path, dependentconceptindex, section 1.3hott_book
K0DS81Z1GMproofproof, section 7.5.2hott_book
lifting, equivalencesconceptindex, section 1.14.1hott_book
type, functionconceptindex, section A.2hott_book
Eilenberg--Mac Lane spaceconceptindex, section 7.10hott_book
universal, property, of set-coequalizerconceptindex, section C.1.2hott_book
game, deductive system asconceptindex, section A.1hott_book
K42482WCR5statementthm, section 1.8hott_book
K4CXJYQ442statementthm, section 3.6hott_book
K4EWD2ZA3Jstatementthm, section 6.2hott_book
K4WPG1F5W8statementlem, section 5.9hott_book
K4XQQK1E9Zdefinitiondefn, section 9.4hott_book
K5CPKT3C91definitiondefn, section C.2hott_book
K5Q0227429statementlem, section 9.8hott_book
K69JSEZGD5statementlem, section 5.4hott_book
function, surjectiveconceptindex, section 6.5hott_book
mathematics, formalizedconceptindex, section 7.10hott_book
type theoryconceptindex, section u1.u1hott_book
K80AG1CAD9statementthm, section B.2.3hott_book
domain, of a functionconceptindex, section A.2hott_book
type, identityconceptindex, section A.12hott_book
function, surjectiveconceptindex, section C.2hott_book
uniqueness, principle, propositional, for functions on a truncationconceptindex, section 6.3hott_book
function, continuous, in classical homotopy theoryconceptindex, section u1.u1hott_book
loop space, iteratedconceptindex, section 7hott_book
real numbers, Dedekindconceptindex, section B.4hott_book
K9MYC99TS9definitiondefn, section C.2hott_book
accessibilityconceptindex, section C.5hott_book
K9XRVFRNDQproofproof, section C.1.3hott_book
KA6AA6DEYTstatementlem, section 6.5hott_book
KACT31EKF9statementthm, section 8.8hott_book
iterator, for natural numbersconceptindex, section A.12.3hott_book
linear orderconceptindex, section B.2.1hott_book
discrete, spaceconceptindex, section u1.u8hott_book
KCBPT2M21Xdefinitiondefn, section 9.1hott_book
KD4RJ5V910exerciseex, section 5.13hott_book
KDMK078JEBstatementcor, section 7.5hott_book
KE1MJSNHA7statementthm, section 1.7hott_book
KEBVH9N9R9proofproof, section 3.2hott_book
Eilenberg--Mac Lane Spacesstatementthm, section 7.10hott_book
KEJHQK931Wproofproof, section B.2.2hott_book
constant, explicitconceptindex, section 4.1hott_book
KF39M6S5GKproofproof, section 6.5hott_book
KFCZTWB1H8proofproof, section 6.3hott_book
inhabited typeconceptindex, section 9.3hott_book
irreflexivity, of well-founded relationconceptindex, section C.4hott_book
four-color theoremconceptindex, section u1.u6hott_book
nounconceptindex, section 9.10hott_book
loop, $n$-conceptindex, section 5.4hott_book
KK7R33Q6BCproofproof, section C.2hott_book
adjectiveconceptindex, section 9.10hott_book
homotopy, inductionconceptindex, section 8.8hott_book
type, unitconceptindex, section 8.3hott_book
formation ruleconceptindex, section 4.2.4hott_book
witness, to the truth of a propositionconceptindex, section A.11hott_book
bimoduleconceptindex, section B.6hott_book
type, emptyconceptindex, section 8.3hott_book
KQ7SYTBZN4exerciseex, section 6.7hott_book
axiom, Streicher's Axiom Kconceptindex, section 6.7hott_book
disjoint, basepointconceptindex, section 5.5hott_book
equivalence, properties ofconceptindex, section 3.5hott_book
inductive, type familyconceptindex, section 8.7hott_book
group, abelianconceptindex, section 3.1hott_book
KR5A88Z8P1proofproof, section 7.8hott_book
type, dependent functionconceptindex, section 4.2.4hott_book
KRGYE8J3B0statementthm, section 6.1hott_book
KS8S6MFS00definitiondefn, section C.3hott_book
fiberconceptindex, section 7.4hott_book
``continuity'' of functions in type theoryconceptindex, section 9.11hott_book
KVBZX893CSproofproof, section B.5hott_book
metatheoryconceptindex, section 4.4hott_book
type, universe, Tarski-styleconceptindex, section A.12.3hott_book
KXAKAT92BXdefinitiondefn, section C.5hott_book
KXH10CQQSKstatementthm, section C.4hott_book
KXVD5P73DDstatementcor, section 6.5hott_book
universal propertyconceptindex, section 8.2hott_book
KZDS3DGR8Bproofproof, section C.4hott_book
KZQ155TQ39statementlem, section C.2hott_book
KZQ8BJYMCJstatementlem, section 3.2hott_book
type, unitconceptindex, section A.8hott_book
compactness, metricconceptindex, section B.5hott_book
variable, and substitutionconceptindex, section sec:formal-prelimhott_book
M0W9CHF2N1statementcor, section 6.7hott_book
univalence axiomconceptindex, section 3.9hott_book
M2M13SQCFKproofproof, section C.1.4hott_book
associativityconceptindex, section 5.11hott_book
M2ZREB7BB8statementlem, section 9.11hott_book
discconceptindex, section 5.7hott_book
M3SDKJAH2Jdefinitiondefn, section 6.4hott_book
M433T73QQ2proofproof, section 6.6hott_book
variableconceptindex, section 8.6hott_book
M45GFTT7XAproofproof, section 9.9hott_book
automorphism, fixed-point-freeconceptindex, section u1.u7hott_book
M54CP9716Dexerciseex, section 9.11hott_book
M5E5C9Q0F3statementthm, section 2.2hott_book
M5VMGMH57Wproofproof, section 7.1.3hott_book
relation, antisymmetricconceptindex, section B.6hott_book
function extensionality, proof from interval typeconceptindex, section 5.3hott_book
$(\infty,1)$-toposconceptindex, section 2.9hott_book
programmingconceptindex, section u1.u1hott_book
toposconceptindex, section 6.7hott_book
Whitehead's, principleconceptindex, section 7.8hott_book
Conway's simplicity theoremstatementthm, section B.6hott_book
equality, propositionalconceptindex, section A.1hott_book
mathematics, predicativeconceptindex, section 8.6hott_book
The 2-out-of-3 propertystatementthm, section 3.7hott_book
proofconceptindex, section A.11hott_book
rounded, Dedekind cutconceptindex, section B.2hott_book
transport, in coproduct typesconceptindex, section 1.12hott_book
formal, type theoryconceptindex, section 4hott_book
MANZK0DCFRstatementlem, section 7.1.4hott_book
MAPW9M43FNexampleeg, section 2.8hott_book
MAZ1X1Q3HWproofproof, section 6.2hott_book
MB16RPACJRexerciseex, section 5.13hott_book
MB51EK9P0Aproofproof, section 3.4hott_book
MBEZN38YNAstatementlem, section 9.1hott_book
MBV9J17AEJproofproof, section 5.9hott_book
MBVQPKQJ4Ndefinitiondefn, section B.5hott_book
MCMR5D0B08definitiondefn, section B.2hott_book
induction principle, for natural numbersconceptindex, section A.9hott_book
term, closedconceptindex, section 4.4hott_book
acceptanceconceptindex, section B.5hott_book
type, higher inductiveconceptindex, section 5hott_book
induction principle, for $\Sn^2$conceptindex, section 5.4hott_book
successor, isomorphism on $\Z$conceptindex, section 7.1.3hott_book
MH7NDQ3D4Qproofproof, section C.1.5hott_book
coherenceconceptindex, section 8.5hott_book
MHA3M1D0CKstatementlem, section 9.11hott_book
MHM08JSKESstatementlem, section B.3.2hott_book
MHNNAXQNP4statementcor, section 7.1.5hott_book
trueconceptindex, section A.11hott_book
law, de Morgan'sconceptindex, section A.11hott_book
MKK5489X5Fproofproof, section B.6hott_book
functor, loop spaceconceptindex, section 7.4hott_book
type, coproductconceptindex, section A.8hott_book
compactness, Heine-Borelconceptindex, section B.5hott_book
multiplication, of natural numbersconceptindex, section A.12.3hott_book
logic, constructiveconceptindex, section u1.u7hott_book
computation rule, for identity typesconceptindex, section A.12.1hott_book
MPSKHHE3AMstatementlem, section 1.4hott_book
MPTD96YR4Aproofproof, section 3.1hott_book
resizingconceptindex, section 9.11hott_book
MQE9H0WSJ1exerciseex, section 8.8hott_book
recursion principle, for Cauchy realsconceptindex, section B.3.2hott_book
half adjoint equivalenceconceptindex, section 3.2hott_book
MR0S0628TZstatementlem, section 1.4hott_book
indiscernibility of identicalsconceptindex, section A.12hott_book
MS0DNA8507proofproof, section 5.10hott_book
MS3N7ZTYSGexerciseex, section A.12.3hott_book
cocomplete categoryconceptindex, section C.1.1hott_book
MS9338SNVWstatementlem, section 1.1hott_book
constructivityconceptindex, section u1.u7hott_book
MSGVAMQH0Tproofproof, section 5.8hott_book
type, negativeconceptindex, section 1.12hott_book
MTBW9ZRFS7proofproof, section 6.2hott_book
MTH4BCRWVGexerciseex, section 5.13hott_book
recursion principle, for natural numbersconceptindex, section A.9hott_book
MV5D7Z68WBproofproof, section B.6hott_book
successor, isomorphism on $\Z$conceptindex, section 7.1.1hott_book
Cauchy, approximation, type ofconceptindex, section B.3.2hott_book
scopeconceptindex, section A.6hott_book
MWFBY7KW27exerciseex, section 9.11hott_book
bi-invertible functionconceptindex, section 3.3hott_book
induction principle, for productconceptindex, section A.5hott_book
MXGGYSX3NAproofproof, section 1.12hott_book
pentagon, Mac Laneconceptindex, section 2.2hott_book
natural numbersconceptindex, section 4.2.9hott_book
inverse, in a groupconceptindex, section 5.11hott_book
coconeconceptindex, section 6.4hott_book
MZ6J63VQKPproofproof, section 6.3hott_book
set theory, Zermelo--Fraenkelconceptindex, section Chott_book
N020KPAVVEexerciseex, section B.6hott_book
N0QE9AHKF8statementcor, section C.3hott_book
N0X986X11Xdefinitiondefn, section C.3hott_book
N1E360VKKRstatementlem, section 5.9hott_book
N39HSACRCAproofproof, section 6.3hott_book
fundamental, pregroupoidconceptindex, section 7.7hott_book
type, identityconceptindex, section 4.2.10hott_book
absolute valueconceptindex, section B.3.3hott_book
Elementary Theory of the Category of Setsconceptindex, section C.1.5hott_book
N5G3C4AZ4Nexerciseex, section C.5hott_book
algebra, for an endofunctorconceptindex, section 8.4hott_book
power setconceptindex, section C.1.4hott_book
Lawvereconceptindex, section B.6hott_book
proof, assistant, Agdaconceptindex, section A.12.3hott_book
induction principle, for interval typeconceptindex, section 5.3hott_book
N6ABWTNSEXexerciseex, section C.5hott_book
N6VDJFNH5Hstatementlem, section C.1.2hott_book
N7X1WWBWWJproofproof, section 1.6hott_book
pullbackconceptindex, section 6.1hott_book
adjoint, functorconceptindex, section C.1.4hott_book
uniqueness, principle, propositional, for homotopy $\w$-typesconceptindex, section 8.5hott_book
type, homotopy-inductiveconceptindex, section 8.5hott_book
N8QMKH60PSstatementlem, section C.5hott_book
Equivalence inductionstatementcor, section 8.8hott_book
Second proofproofproof, section 1.3hott_book
vary along a path constructorconceptindex, section 5.2hott_book
induction principle, for accessibilityconceptindex, section C.3hott_book
quantifier, existentialconceptindex, section A.11hott_book
NA4JEQBDV4exerciseex, section 9.11hott_book
NA963GCNWQstatementthm, section 6.2hott_book
NAHHJQ015Gstatementlem, section 9.3hott_book
NARC2T6R44statementthm, section 6.2hott_book
generation, of a type, inductiveconceptindex, section 8.8hott_book
squaring functionconceptindex, section B.3.3hott_book
retract, of a typeconceptindex, section 3.9hott_book
path, $n$-conceptindex, section 5.13hott_book
mathematics, constructiveconceptindex, section B.5hott_book
completion, Rezkconceptindex, section C.1.3hott_book
NDV5N1AXWPproofproof, section 2.5hott_book
sequenceconceptindex, section B.4hott_book
mathematics, classicalconceptindex, section 2hott_book
Cauchy, sequenceconceptindex, section B.6hott_book
relation, antisymmetricconceptindex, section 2.1hott_book
NE5QWHVX16exerciseex, section A.12.3hott_book
NE844MA1MSdefinitiondefn, section 1.14hott_book
Cauchy, sequenceconceptindex, section B.4hott_book
rule, formationconceptindex, section 4.2.4hott_book
NG7BZZ9ATXexerciseex, section C.5hott_book
NG8DHQTR3Vdefinitiondefn, section 2.8hott_book
attaching mapconceptindex, section 5.6hott_book
NGM2RZ4JSXproofproof, section 2.9hott_book
NGMEGPC9XVproofproof, section 2.2hott_book
NGZVZ1ANRHproofproof, section 3.9hott_book
NH1GGMQJ5Jstatementthm, section 7.1.6hott_book
NH1TW632F3proofproof, section 6.4hott_book
NJ7BRMPE42statementlem, section 6.5hott_book
theorem, Whitehead'sconceptindex, section 7.8hott_book
computation rule, propositional, for identities between functionsconceptindex, section 1.9hott_book
fundamental, groupconceptindex, section 1hott_book
type, 2-sphereconceptindex, section 5.4hott_book
NMVGVZPM5Sproofproof, section 7.9hott_book
univalence axiomconceptindex, section 4.3.1hott_book
NN54G1EKY4statementlem, section 6.5hott_book
pattern matchingconceptindex, section 8.6hott_book
NNQXQPBEM2proofproof, section 3.7hott_book
structural, recursionconceptindex, section 4.1hott_book
NPN606JQ0Cstatementthm, section 8.5hott_book
associativity, of joinconceptindex, section 7.5.3hott_book
theorem, odd-orderconceptindex, section u1.u5hott_book
NSEA890YZ0statementthm, section 3.3hott_book
NSW60C33DEexerciseex, section 1.15hott_book
negationconceptindex, section 9.4hott_book
NTDCQA6V93statementlem, section 6.6hott_book
Martin-L\ofconceptindex, section 4.4hott_book
NV829PY6QEexerciseex, section 2.9hott_book
NVAKEBHKB0exerciseex, section 1.15hott_book
NVQQYXT5Z1proofproof, section 6.7hott_book
discrete, spaceconceptindex, section 9.1hott_book
excluded middleconceptindex, section B.4hott_book
pattern matchingconceptindex, section A.10hott_book
NWY4PD995Sproofproof, section 3.6hott_book
Quillen model categoryconceptindex, section u1.u2hott_book
excluded middleconceptindex, section B.5hott_book
path, $n$-conceptindex, section 5.4hott_book
NYKDDQVBK9statementlem, section B.3.2hott_book
functionconceptindex, section A.2hott_book
NZVM5Z0DGMproofproof, section 7.3hott_book
bargainingconceptindex, section 2.6hott_book
$\eta $-expansionconceptindex, section A.2hott_book
propositional, resizingconceptindex, section 8.6hott_book
P0SY34RGYTproofproof, section C.4hott_book
P1C4BJWATPexerciseex, section 6.7hott_book
synthetic mathematicsconceptindex, section 1hott_book
precategory, product ofconceptindex, section 2.5hott_book
P27ZHXWFX1exerciseex, section 6.7hott_book
decidable, equalityconceptindex, section A.11hott_book
P2PWSWNR2Jstatementcor, section 9.11hott_book
Proof of \cref{thm:flattening}proofproof, section 5.12hott_book
P3195ZF1W4statementlem, section C.3hott_book
P34V7VFYRQstatementcor, section 7.2hott_book
P38JF2T0A5statementthm, section 6.1hott_book
type, productconceptindex, section 1.6hott_book
rewriting ruleconceptindex, section 4.4hott_book
bargainingconceptindex, section B.3hott_book
path, dependentconceptindex, section 5.2hott_book
P6602S33KMproofproof, section B.3.2hott_book
excluded middleconceptindex, section 6.2hott_book
P79M82DFXGproofproof, section 5.10hott_book
homotopy, group, of sphereconceptindex, section 7hott_book
category, product ofconceptindex, section 2.5hott_book
simplicial, setsconceptindex, section u1.u2hott_book
type, inductive, generalizationsconceptindex, section 8.7hott_book
collection, strongconceptindex, section C.5hott_book
confluenceconceptindex, section 4.4hott_book
order, linearconceptindex, section B.2.1hott_book
unique, factorization systemconceptindex, section 6.7hott_book
PANS8WCWJ0statementlem, section B.5hott_book
transitivity, of equalityconceptindex, section 1.1hott_book
PBBECTKKR7statementthm, section B.5hott_book
constructorconceptindex, section 8.6hott_book
PBXVSWCMQ8proofproof, section 7.1.5hott_book
PD7BB6C36Astatementthm, section 8.3hott_book
hypothesisconceptindex, section A.11hott_book
nonempty subsetconceptindex, section C.4hott_book
PE4TS2GG2Sdefinitiondefn, section 3.3hott_book
type, smallconceptindex, section u1.u3hott_book
universal, property, of $\Sn^n$conceptindex, section 5.5hott_book
PFN7B9ZKMRproofproof, section B.3.2hott_book
real numbersconceptindex, section Bhott_book
propositional, resizingconceptindex, section C.5hott_book
induction principle, for integersconceptindex, section 5.10hott_book
PH19CW0F2Gexerciseex, section B.6hott_book
total, relationconceptindex, section B.6hott_book
PH5HH3HVQMstatementlem, section 6.3hott_book
PH5TXCMXYMproofproof, section 3.7hott_book
PJH8ATJTVJproofproof, section 3.3hott_book
amalgamated free productconceptindex, section 7.7.2hott_book
kernel, pairconceptindex, section 7.7.2hott_book
PJVPDPGH4Aproofproof, section 6.3hott_book
PMV6TA5G8Sstatementcor, section C.2hott_book
axiom, versus rulesconceptindex, section 1.5hott_book
PN36HW0257exerciseex, section C.5hott_book
PNDKWSVXXGproofproof, section B.3.3hott_book
convertibility of termsconceptindex, section 4.1hott_book
weakly linear orderconceptindex, section B.2.1hott_book
PQ53JKVC68statementlem, section 7.4hott_book
recursion principle, for $\Sn^2$conceptindex, section 5.4hott_book
PRCMA2K917proofproof, section 9.2hott_book
universal, property, of dependent pair typeconceptindex, section 5.12hott_book
PSXCC1DVRMproofproof, section 7.4hott_book
PT7BEHRQQWexampleeg, section 2.1hott_book
automorphism, fixed-point-freeconceptindex, section 9.2hott_book
PTZYW1ADSEexerciseex, section B.6hott_book
computation rule, for inductive typesconceptindex, section 8.6hott_book
weak equivalence, of precategoriesconceptindex, section C.4hott_book
PWSXHFPDYYexampleeg, section 7.7.2hott_book
univalence axiomconceptindex, section 1.15hott_book
PX1W3G9K5Kexerciseex, section 6.7hott_book
PX32TV7S2Kproofproof, section 5.9hott_book
apartnessconceptindex, section B.6hott_book
group, abelianconceptindex, section 7.7.2hott_book
The Freudenthal suspension theoremstatementthm, section 7.6hott_book
toposconceptindex, section C.1.5hott_book
sequenceconceptindex, section 1hott_book
PZ9NJW45F1proofproof, section 2.9hott_book
setconceptindex, section 2.1hott_book
logic, of mere propositionsconceptindex, section 9.10hott_book
PZX4YW9SBVexerciseex, section 8.8hott_book
Q0VHC1DX3Kexerciseex, section 9.11hott_book
Q22ZQ51169exerciseex, section 9.11hott_book
programmingconceptindex, section A.2hott_book
Q2NXVEPNHXproofproof, section 2.4hott_book
Q30V9A6QBYproofproof, section B.5hott_book
Q3EWZ6P22Ydefinitiondefn, section 8.4hott_book
Q3K07ZK32Cproofproof, section 6.7hott_book
$(\infty,1)$-toposconceptindex, section 7.7.2hott_book
group, abelianconceptindex, section 7.10hott_book
fundamental, groupconceptindex, section 7hott_book
adverbconceptindex, section 6.7hott_book
automorphism, of $\bool$, nonidentityconceptindex, section 5.13hott_book
axiom, of choiceconceptindex, section C.1.5hott_book
axiom, Streicher's Axiom Kconceptindex, section A.12.3hott_book
free, complete metric spaceconceptindex, section B.3hott_book
proofconceptindex, section A.1hott_book
definition, of adverbsconceptindex, section 9.10hott_book
setconceptindex, section Chott_book
functionconceptindex, section 1.2hott_book
Q8A6M6K1NDproofproof, section 5.4hott_book
equivalence, properties ofconceptindex, section 3.7hott_book
QBC8KTVVGJexerciseex, section 8.8hott_book
Fubini theorem for colimitsconceptindex, section 7.5.3hott_book
axiom, versus rulesconceptindex, section A.1hott_book
QD5WB8TNR5exampleeg, section 7.7.1hott_book
stability, of images under pullbackconceptindex, section 6.6hott_book
irreflexivity, of $<$ in a fieldconceptindex, section B.2.1hott_book
pattern matchingconceptindex, section A.12.3hott_book
axiom, of choiceconceptindex, section C.4hott_book
$\w$-typeconceptindex, section 8.3hott_book
QEQABKCQZKstatementthm, section 6.1hott_book
$\infty$-groupoid, fundamentalconceptindex, section 1hott_book
type, limitconceptindex, section 5.8hott_book
QHPWVHDB0Astatementlem, section 7.1.3hott_book
decidable, equalityconceptindex, section 7.10hott_book
associativity, in a monoidconceptindex, section 5.11hott_book
QJRJJ9CTHSdefinitiondefn, section 7.5.2hott_book
uniqueness, principle, propositional, for functions on $\nat$conceptindex, section 8.1hott_book
Archimedean principle for $\RD$statementthm, section B.2.1hott_book
ordinal, pseudo-conceptindex, section B.6hott_book
QKM2W2RGPAproofproof, section C.3hott_book
induction principle, for dependent pair typeconceptindex, section A.6hott_book
logic, constructive vs classicalconceptindex, section A.11hott_book
QNJFG2H90Sdefinitiondefn, section 6.6hott_book
QP7P25R3NFstatementthm, section C.4hott_book
associativity, of functor compositionconceptindex, section 2.2hott_book
classical, homotopy theoryconceptindex, section 7.1.2hott_book
induction principleconceptindex, section 8.1hott_book
total, spaceconceptindex, section 7.1.2hott_book
QRBTN9DGQWstatementthm, section B.3.3hott_book
QRG7V2YFSSproofproof, section 6.1hott_book
interchange lawconceptindex, section 2.2hott_book
monomorphismconceptindex, section C.1.4hott_book
associativity, of path concatenation, coherence ofconceptindex, section 1.1hott_book
computation rule, for type of booleansconceptindex, section 8.1hott_book
axiom, of $\Delta_0$-separationconceptindex, section C.5hott_book
QV984NNYFRstatementlem, section 9.3hott_book
free, algebraic structureconceptindex, section 5.11hott_book
angerconceptindex, section 6.2hott_book
QVW3TZQ7YKdefinitiondefn, section 3.7hott_book
$\lambda$-calculusconceptindex, section u1.u1hott_book
QW32WY7032statementthm, section B.3.4hott_book
propositional, resizingconceptindex, section C.1.4hott_book
uniqueness, principle, propositional, for functions on $\w$-typesconceptindex, section 8.3hott_book
QXBGY020P0statementlem, section 1.3hott_book
strict, positivityconceptindex, section B.6hott_book
strict, positivityconceptindex, section 5.13hott_book
QYK11QG66Zstatementlem, section 6.5hott_book
QZ2WBH1KA2proofproof, section 1.11hott_book
center, of a categoryconceptindex, section 3.1hott_book
R06Y3YQGSFdefinitiondefn, section 7.4hott_book
mathematics, constructiveconceptindex, section B.2hott_book
indiscernibility of identicalsconceptindex, section 1.3hott_book
R0MMTV6W6Estatementcor, section 7.8hott_book
mathematics, classicalconceptindex, section B.6hott_book
R1Y4V4CSY4statementthm, section 6.3hott_book
R2DZ4FPF8Hproofproof, section C.1.3hott_book
typical ambiguityconceptindex, section C.3hott_book
R4GKSBKMB8proofproof, section 7.5.3hott_book
First proofproofproof, section 1.1hott_book
uniqueness, principle, propositional, for univalenceconceptindex, section 1.10hott_book
normalization, strongconceptindex, section 4.4hott_book
group, abelian, exact sequence ofconceptindex, section 7.4hott_book
excluded middleconceptindex, section A.11hott_book
hub and spokeconceptindex, section 6.3hott_book
axiom, of choice, type-theoreticconceptindex, section 1.15hott_book
quantifier, boundedconceptindex, section C.5hott_book
total, spaceconceptindex, section 1.7hott_book
ordinalconceptindex, section B.6hott_book
total, spaceconceptindex, section 7.5.3hott_book
RA80R5C1H3proofproof, section 7.1.4hott_book
RAXK4K0BVTstatementlem, section C.1.2hott_book
setconceptindex, section 6.1hott_book
RBDXKGCNXEexerciseex, section 9.11hott_book
Lawvereconceptindex, section 8.8hott_book
The Yoneda lemmastatementthm, section 2.5hott_book
RC25R793HAstatementthm, section 2.4hott_book
RCAPP9BP2Kexerciseex, section A.12.3hott_book
universal, property, of pushoutconceptindex, section 5.8hott_book
loopconceptindex, section 1.1hott_book
RCXSTCFN8Bproofproof, section C.2hott_book
RDS2J8C321proofproof, section B.5hott_book
type, coproductconceptindex, section 4.2.6hott_book
limited principle of omniscienceconceptindex, section B.6hott_book
equipped withconceptindex, section A.6hott_book
RG027A74XRexampleeg, section 9.1hott_book
wedgeconceptindex, section 7.6hott_book
RH3253PGBPexerciseex, section A.12.3hott_book
inaccessible cardinalconceptindex, section u1.u7hott_book
locatednessconceptindex, section B.2hott_book
algorithmconceptindex, section 1hott_book
RJCPWHSGTDstatementlem, section C.1.2hott_book
covering space, universalconceptindex, section 7.1.3hott_book
fundamental, pregroupoidconceptindex, section 2.9hott_book
semigroupconceptindex, section A.11hott_book
monadconceptindex, section 6.7hott_book
theorem, Diaconescu'sconceptindex, section C.1.5hott_book
mathematics, formalizedconceptindex, section 1.1hott_book
RKK66WXQR4statementlem, section 5.4hott_book
RKPVFM7BWGexerciseex, section 6.7hott_book
RKQS6EVFJFstatementcor, section 7.1.6hott_book
Segal, categoryconceptindex, section 2.9hott_book
operadconceptindex, section 1.1hott_book
classical, category theoryconceptindex, section 2hott_book
analysis, constructiveconceptindex, section B.5hott_book
constructive, analysisconceptindex, section B.5hott_book
contractible, typeconceptindex, section 9.11hott_book
surreal numbersconceptindex, section B.6hott_book
RNRR9CNV53statementcor, section 6.5hott_book
RP0Q1FWBJ8statementlem, section 2.5hott_book
factorization, stability under pullbackconceptindex, section 6.6hott_book
RR00VGH722proofproof, section 6.1hott_book
induction principle, for a modalityconceptindex, section 6.7hott_book
completion, Rezkconceptindex, section C.5hott_book
proof, assistantconceptindex, section u1.u1hott_book
pushout, of setsconceptindex, section 5.9hott_book
falseconceptindex, section A.11hott_book
hub and spokeconceptindex, section 7.7.2hott_book
RVT0BB17R4proofproof, section 2.9hott_book
set-coequalizerconceptindex, section C.1.2hott_book
contravariant functorconceptindex, section 8.6hott_book
natural numbers, as homotopy-initial algebraconceptindex, section 8.4hott_book
RX4PZSENJ6statementlem, section 1.1hott_book
mere propositionconceptindex, section 9.10hott_book
RXSNFJ5TXVexerciseex, section 1.15hott_book
diagramconceptindex, section 6.7hott_book
univalence axiomconceptindex, section u1hott_book
abuse, of languageconceptindex, section 9.10hott_book
RYXMTBNCDHproofproof, section 7.6hott_book
RZF3VC3Y6Wproofproof, section 5.5hott_book
RZHNG4QPK7statementlem, section 2.2hott_book
finite, sets, family ofconceptindex, section A.4hott_book
theorem, Hedberg'sconceptindex, section 9.11hott_book
skeletal categoryconceptindex, section 2.1hott_book
S04V664XS0definitiondefn, section 2.7hott_book
S0CT37YBNVexerciseex, section B.6hott_book
Second proofproofproof, section 1.3hott_book
Scottconceptindex, section 8.8hott_book
S1E6R7SS06statementthm, section 8.5hott_book
S1YHT7G4HTproofproof, section 2.4hott_book
locally cartesian closed categoryconceptindex, section C.1.4hott_book
computation rule, for $\w$-typesconceptindex, section 8.3hott_book
induction principle, for connected mapsconceptindex, section 6.5hott_book
S6535MJQY3statementlem, section 6.5hott_book
spanconceptindex, section 5.8hott_book
theorem, Schroeder--Bernsteinconceptindex, section C.2hott_book
order, non-strictconceptindex, section B.3.3hott_book
S8GDP0QT6Nstatementcor, section B.3.2hott_book
variable, in contextconceptindex, section sec:formal-prelimhott_book
function, injectiveconceptindex, section 6.6hott_book
theorem, van Kampenconceptindex, section 2.9hott_book
S9H1GC4H1Rstatementthm, section 6.6hott_book
S9N7498P0Vstatementthm, section 6.6hott_book
pathconceptindex, section 1.1hott_book
computation rule, propositionalconceptindex, section 5.7hott_book
zeroconceptindex, section 8.3hott_book
SBR2WF31GZstatementlem, section B.2.3hott_book
``functoriality'' of functions in type theoryconceptindex, section 1.4hott_book
type, pointedconceptindex, section 5.4hott_book
SD3784621Fexerciseex, section 5.13hott_book
order, strictconceptindex, section B.2.1hott_book
SDBKY7MJ96exerciseex, section C.5hott_book
logic, of mere propositionsconceptindex, section 9.6hott_book
SFCJ9PQKZBstatementcor, section 6.1hott_book
SFDAPD49K8proofproof, section C.3hott_book
computation rule, for natural numbersconceptindex, section A.9hott_book
axiom, of choice, countableconceptindex, section B.4hott_book
universal, property, of pushoutconceptindex, section 5.9hott_book
type, dependent pairconceptindex, section 1.15hott_book
SJ6WPWRKDCexerciseex, section B.6hott_book
definitionconceptindex, section 4.2.11hott_book
Encode-decode for Loop Spacesstatementlem, section 7.9hott_book
cyclic groupconceptindex, section 7hott_book
fundamental, groupconceptindex, section 7.7hott_book
programmingconceptindex, section 6.7hott_book
open, problemconceptindex, section B.6hott_book
SN1JDB45KBstatementthm, section 6.7hott_book
iterated loop spaceconceptindex, section 1.1hott_book
type, of listsconceptindex, section B.5hott_book
associativity, of function compositionconceptindex, section A.12.3hott_book
computation ruleconceptindex, section 4.2.4hott_book
generation, of a type, inductiveconceptindex, section 8.1hott_book
mathematics, classicalconceptindex, section 2.9hott_book
SQWDCWYJ45exampleeg, section 1.4hott_book
SR4QV9YRPMexerciseex, section 7.10hott_book
SRTAKA0Y5Xproofproof, section 5.4hott_book
SRYW98XH3Gproofproof, section 6.5hott_book
SRZK9DRGKWexerciseex, section 9.11hott_book
transitivity, of $\leq$ for realsconceptindex, section B.2.1hott_book
weak equivalence, of precategoriesconceptindex, section 2.9hott_book
discrete, spaceconceptindex, section u1.u7hott_book
SSSEKQ5DY1statementthm, section 1.6hott_book
multiplication, of ordinal numbersconceptindex, section C.5hott_book
ST25MDDEGBexerciseex, section 1.15hott_book
mathematics, classicalconceptindex, section C.4hott_book
abuse, of notationconceptindex, section u1.u3hott_book
STP60CQ6X4statementthm, section 8.4hott_book
SVSAAKCEPVexampleeg, section 7.7.1hott_book
Sketch of proofproofproof, section C.5hott_book
pointwise, functionalityconceptindex, section A.12.3hott_book
mathematics, predicativeconceptindex, section Chott_book
SY89ZZWY5Qstatementcor, section C.2hott_book
mathematics, classicalconceptindex, section 9.3hott_book
SYVYGDM29Fstatementthm, section 1.6hott_book
induction principle, for suspensionconceptindex, section 5.5hott_book
SZJCP3APPPdefinitiondefn, section 6.4hott_book
SZNBW926RVstatementthm, section 3.2hott_book
SZY6MZSHMPstatementlem, section C.2hott_book
T0A2KPE7HJproofproof, section 9.1hott_book
T136WJ3V4Aproofproof, section 9.9hott_book
T18HB966C0exerciseex, section 8.8hott_book
torusconceptindex, section 5.6hott_book
T1PTXT7C1Jdefinitiondefn, section 2.5hott_book
equality, reflexivity ofconceptindex, section 1.1hott_book
Yoneda, lemmaconceptindex, section 8.8hott_book
proof, assistant, Coqconceptindex, section A.12.3hott_book
T1YZFB297Aexerciseex, section 9.11hott_book
$\lambda$-abstractionconceptindex, section A.2hott_book
Galois, extensionconceptindex, section 2.6hott_book
first-order, logicconceptindex, section 9.10hott_book
eliminatorconceptindex, section 4.2.4hott_book
T3DZDGK7FSproofproof, section 2.4hott_book
T3JF4QZGTHstatementthm, section 4.4hott_book
T3KQ18X9MKproofproof, section 6.6hott_book
equality, judgmentalconceptindex, section sec:formal-prelimhott_book
CW complexconceptindex, section 7.7.2hott_book
homotopy, topologicalconceptindex, section 1hott_book
encode-decode methodconceptindex, section 7.7.2hott_book
T4QJ8WH2XTdefinitiondefn, section 3.7hott_book
univalence axiomconceptindex, section 2.1hott_book
mathematics, predicativeconceptindex, section C.5hott_book
mutual inductive typeconceptindex, section 8.7hott_book
T5W0JSQVSJstatementlem, section 9.11hott_book
T6TNW370HEdefinitiondefn, section 1.4hott_book
T71QBA0N94proofproof, section 7.6hott_book
spanconceptindex, section 7.5.1hott_book
symmetry, of equalityconceptindex, section 1.1hott_book
$\alpha $-conversionconceptindex, section sec:formal-prelimhott_book
completion, Dedekindconceptindex, section B.2.3hott_book
covering space, universalconceptindex, section 7.1.2hott_book
Klein bottleconceptindex, section 5.6hott_book
T97NG45WA0statementthm, section 2.9hott_book
Postnikov towerconceptindex, section 6.3hott_book
TAQ3XK5XMHdefinitiondefn, section 9.7hott_book
rounded, Dedekind cutconceptindex, section B.6hott_book
axiom, subset collectionconceptindex, section C.5hott_book
TAZW2VATXYstatementlem, section 9.8hott_book
TBE9Y2J4P6proofproof, section 7.6hott_book
TBNG8V6ZM6proofproof, section C.3hott_book
cut, Dedekindconceptindex, section B.4hott_book
order, weakly linearconceptindex, section B.2.1hott_book
TCH0CQHKWYproofproof, section 7.1.6hott_book
TCNJ92EH3Vstatementlem, section 2.4hott_book
TCRE951H2Jexerciseex, section 5.13hott_book
inductive, definitionconceptindex, section 8hott_book
TEKYY50SD3definitiondefn, section 3.2hott_book
Sketch of proofproofproof, section 6.6hott_book
TFJXFSQXB1statementlem, section 5.12hott_book
induction principle, for $\Sn^1$conceptindex, section 5.2hott_book
isomorphism, transfer acrossconceptindex, section 8.2hott_book
interval, arithmeticconceptindex, section B.6hott_book
THFC13CHHZproofproof, section C.3hott_book
TJ23FTC5E1definitiondefn, section 5.10hott_book
TK0RBSE5TVstatementlem, section 1.11hott_book
TK32X4P39Fstatementthm, section 1.11hott_book
TKGK6PPT1Sproofproof, section C.5hott_book
TKS19P6XR2statementcor, section 6.3hott_book
TM8G57S5FGproofproof, section 3.1hott_book
TMAYBDCY44exerciseex, section C.5hott_book
TMMZPFV9MAproofproof, section C.2hott_book
TN0MYQTP6Qstatementlem, section 3.2hott_book
TNAE9CC1A9proofproof, section C.3hott_book
TNKP3CQ05Eproofproof, section 3.8hott_book
purelyconceptindex, section 6.7hott_book
parenthesesconceptindex, section A.2hott_book
Schroeder--Bernstein theoremconceptindex, section C.2hott_book
variableconceptindex, section A.4hott_book
strong, normalizationconceptindex, section 4.4hott_book
induction principle, for type of booleansconceptindex, section A.8hott_book
cut, Dedekindconceptindex, section Bhott_book
TRSQ7DT8ENexerciseex, section 6.7hott_book
path, $n$-conceptindex, section 1.15hott_book
fundamental, theorem of Galois theoryconceptindex, section 2.6hott_book
pattern matchingconceptindex, section 4.4hott_book
unit, law for path concatenationconceptindex, section 1.1hott_book
TW1HGNESENdefinitiondefn, section 2.5hott_book
pullbackconceptindex, section C.1.1hott_book
TX6AYQVD00proofproof, section B.2.2hott_book
integersconceptindex, section 7.1.2hott_book
Second proofproofproof, section 1.2hott_book
TY6XHF0VGPexerciseex, section A.12.3hott_book
TYBE9W8VN5statementthm, section 7.6hott_book
TYD5211ZVHproofproof, section 1.11hott_book
TZDM56QH62statementlem, section C.2hott_book
universal, property, of a modalityconceptindex, section 6.7hott_book
homotopy, topologicalconceptindex, section u1.u1hott_book
strict, orderconceptindex, section B.2.1hott_book
computation rule, for natural numbersconceptindex, section 8.1hott_book
V1FAE01SANexerciseex, section 8.8hott_book
V1HDS219HNstatementlem, section 5.5hott_book
uniqueness, principle, propositional, for functions on a pushoutconceptindex, section 5.8hott_book
de Morgan's lawsconceptindex, section A.11hott_book
V3GB37XDKYproofproof, section 7.3hott_book
V3HW3ZC1J4statementlem, section 5.5hott_book
consistencyconceptindex, section 4.4hott_book
V4BVC0T1G5proofproof, section 5.12hott_book
Martin-L\ofconceptindex, section 8.8hott_book
typical ambiguityconceptindex, section B.2hott_book
V4RZRXQDCKproofproof, section 1.7hott_book
modal, operatorconceptindex, section 6.7hott_book
consistencyconceptindex, section 4hott_book
irreflexivity, of $<$ for realsconceptindex, section B.2.1hott_book
Haskellconceptindex, section 6.7hott_book
V7WEGG88WSproofproof, section C.3hott_book
coherenceconceptindex, section 1.1hott_book
V8R7K3CY33statementlem, section 1.2hott_book
limit, of setsconceptindex, section 5.9hott_book
arityconceptindex, section 8.3hott_book
loop spaceconceptindex, section 7.9hott_book
semiringconceptindex, section C.2hott_book
synthetic mathematicsconceptindex, section 7hott_book
VB1AF85H3Bproofproof, section C.4hott_book
VB5GRSQDMNexerciseex, section 2.9hott_book
VBTT7QZMMEstatementlem, section 7.5.2hott_book
collection, subsetconceptindex, section C.5hott_book
VE8REK6V1Vexerciseex, section 8.8hott_book
magmaconceptindex, section A.11hott_book
VEZ710G3DNproofproof, section C.2hott_book
function, embeddingconceptindex, section 6.1hott_book
modality, identityconceptindex, section 6.7hott_book
function, injectiveconceptindex, section C.2hott_book
Schroeder--Bernsteinstatementthm, section C.2hott_book
type, dependent functionconceptindex, section A.4hott_book
homotopy, group, of sphereconceptindex, section 7.5hott_book
axiom, of replacementconceptindex, section C.5hott_book
type, productconceptindex, section A.12.3hott_book
$(\infty,1)$-categoryconceptindex, section 3.9hott_book
VKBD0W7RDQstatementcor, section 4.4hott_book
disjunctionconceptindex, section A.11hott_book
fibrationconceptindex, section 3.7hott_book
quantifierconceptindex, section 9.7hott_book
classical, category theoryconceptindex, section 2.2hott_book
cardinal number, multiplication ofconceptindex, section C.2hott_book
VNZ1A7HFMYproofproof, section 6.6hott_book
foundations, univalentconceptindex, section u1hott_book
projective planeconceptindex, section 5.6hott_book
recursion principle, for truncationconceptindex, section 6.3hott_book
extensional, type theoryconceptindex, section A.12.3hott_book
non-expanding functionconceptindex, section B.3.3hott_book
VQV7BQ8JJ0proofproof, section 5.12hott_book
mathematics, classicalconceptindex, section B.2.1hott_book
$\lambda$-abstractionconceptindex, section A.4hott_book
VS0Y0AKFM9exerciseex, section 6.7hott_book
Sketch of proofproofproof, section 8.5hott_book
VTHXA66TWPproofproof, section C.2hott_book
definition, by pattern matchingconceptindex, section 8.6hott_book
VWF9PDQ08Dproofproof, section C.3hott_book
open, problemconceptindex, section 4.4hott_book
VY0ZFV03AWstatementthm, section C.3hott_book
fundamental, group, of circleconceptindex, section 7hott_book
VYR541AB7Zproofproof, section B.6hott_book
VZ68FBMMXNstatementlem, section 9.11hott_book
VZWNQH0K7Vexerciseex, section 1.15hott_book
VZY22XMJAVexerciseex, section 2.9hott_book
dimension, of path constructorsconceptindex, section 5.1hott_book
W0C5KBPGYYstatementcor, section 6.2hott_book
group, abelianconceptindex, section 7hott_book
order, non-strictconceptindex, section C.2hott_book
W0RCVCGB4Kstatementthm, section 6.2hott_book
constant, definedconceptindex, section 4.1hott_book
quasi-inverseconceptindex, section 3.1hott_book
source, of a path constructorconceptindex, section 5.6hott_book
W18DCJ0K36statementthm, section 6.7hott_book
W1DCY8844Zdefinitiondefn, section 1.1hott_book
univalence axiomconceptindex, section u1.u3hott_book
W2MQJ71AP0exerciseex, section 9.11hott_book
predecessor, isomorphism on $\Z$conceptindex, section 7.1.3hott_book
induction principle, for type of vectorsconceptindex, section 8.7hott_book
image, stability under pullbackconceptindex, section 6.6hott_book
W3CSZ2HZ56exerciseex, section 8.8hott_book
W433QFQP95statementlem, section 5.12hott_book
W46CQ0EXD9statementlem, section 2.4hott_book
irreflexivity, of apartnessconceptindex, section B.2.1hott_book
constructive, set theoryconceptindex, section C.5hott_book
type, of booleansconceptindex, section A.8hott_book
W5F9BK22CMproofproof, section 1.9hott_book
effective, procedureconceptindex, section A.11hott_book
loop spaceconceptindex, section 7.8hott_book
Peanoconceptindex, section 8.8hott_book
W75MYDZWSAexerciseex, section C.5hott_book
W7E5908JPYexampleeg, section 6.1hott_book
type, inductiveconceptindex, section 8.1hott_book
W7WZ9MGJHCexerciseex, section 9.11hott_book
mathematics, classicalconceptindex, section C.1.4hott_book
isomorphism, naturalconceptindex, section 1.4hott_book
WAK5T0DRG9proofproof, section 5.2hott_book
induction principleconceptindex, section A.5hott_book
WAWEK23JDVproofproof, section 9.3hott_book
WBNPHK9V96definitiondefn, section 2.4hott_book
WBWF5KY8ZKproofproof, section 2.4hott_book
imageconceptindex, section 7.4hott_book
WCD9KF1C5Aexerciseex, section 8.8hott_book
WCFKBTSR0Fexerciseex, section 1.15hott_book
function extensionalityconceptindex, section 3.9hott_book
subset, collectionconceptindex, section C.5hott_book
WDJZ0S0SWBproofproof, section 2.5hott_book
truncation, $n$-truncationconceptindex, section 6.3hott_book
loop space, functoriality ofconceptindex, section 7.4hott_book
mathematics, classicalconceptindex, section 9.4hott_book
orthogonal factorization systemconceptindex, section 6hott_book
mathematics, proof-relevantconceptindex, section 1.1hott_book
$\lambda$-abstractionconceptindex, section A.11hott_book
algorithmconceptindex, section u1.u7hott_book
WFKWRWFJ5Estatementthm, section B.5hott_book
CW complexconceptindex, section 5.6hott_book
WGRY7RGRM0definitiondefn, section 3.2hott_book
WH4GGGAK5Wexerciseex, section 5.13hott_book
proof, assistantconceptindex, section 2.9hott_book
WHYEY6C8YBproofproof, section 6.1hott_book
uniqueness, principle, propositional, for a modalityconceptindex, section 6.7hott_book
WK26YYWT3Pproofproof, section B.5hott_book
WK32RHNTY8exampleeg, section B.6hott_book
identity, system, at a pointconceptindex, section 8.8hott_book
WKDCR4T5X4proofproof, section 6.3hott_book
plump, ordinalconceptindex, section C.5hott_book
inductive, hypothesisconceptindex, section A.9hott_book
computation rule, for coproduct typeconceptindex, section A.7hott_book
coincidence, of Cauchy approximationsconceptindex, section B.3hott_book
universe levelconceptindex, section C.3hott_book
colimit, of setsconceptindex, section C.1.1hott_book
WMVNJY4NXCstatementthm, section B.3.3hott_book
recursion principle, for dependent pair typeconceptindex, section A.6hott_book
uniqueness, principle, propositional, for product typesconceptindex, section 1.6hott_book
WNGH0QZD2Sexampleeg, section 2.1hott_book
WP0T4BN0W0proofproof, section 3.2hott_book
extraction of algorithmsconceptindex, section u1.u6hott_book
WPSVQ2CRHZproofproof, section 3.9hott_book
adjoint, equivalenceconceptindex, section 3.9hott_book
WQD78JBR0Zstatementthm, section 6.1hott_book
WQQW8QBVM4statementlem, section 3.2hott_book
completion, Rezkconceptindex, section 2hott_book
mathematics, proof-relevantconceptindex, section 1.4hott_book
propositional, resizingconceptindex, section 9.11hott_book
loop, $n$-conceptindex, section 6hott_book
path, induction basedconceptindex, section A.12.1hott_book
product, of (pre)categoriesconceptindex, section 2.5hott_book
limit, of a Cauchy approximationconceptindex, section B.5hott_book
monoid, freeconceptindex, section 5.11hott_book
WTZMRBPERJproofproof, section B.3.3hott_book
universal, property, of natural numbersconceptindex, section 8.4hott_book
tree, well-foundedconceptindex, section 8.3hott_book
axiom, of choice, type-theoreticconceptindex, section 9.2hott_book
transportconceptindex, section 1.3hott_book
power setconceptindex, section 8.6hott_book
WYA46VH1CEexerciseex, section B.6hott_book
strict, orderconceptindex, section B.3.3hott_book
type, functionconceptindex, section 1.9hott_book
X05FD7VSEZproofproof, section 3.2hott_book
ringconceptindex, section B.1hott_book
X1WV6PM2G2proofproof, section 8.1hott_book
X37MBT5RGDstatementthm, section C.1.4hott_book
mathematics, classicalconceptindex, section A.12.3hott_book
transport, in product typesconceptindex, section 1.6hott_book
computation rule, propositional, for identities between pairsconceptindex, section 1.6hott_book
type theory, intensionalconceptindex, section 1.15hott_book
X4GJ40TJ5Nstatementthm, section 3.9hott_book
X4NMPH4JBMstatementlem, section B.2.1hott_book
setconceptindex, section 6.2hott_book
setoidconceptindex, section 9.11hott_book
$\infty$-groupoidconceptindex, section 8.4hott_book
X5R2HZH98Fproofproof, section 3.2hott_book
type, circleconceptindex, section 5.2hott_book
imageconceptindex, section C.1.2hott_book
proof, by contradictionconceptindex, section A.11hott_book
X6VJ410B2Ystatementcor, section 5.10hott_book
evilconceptindex, section 2.9hott_book
First proofproofproof, section 1.2hott_book
X81B4B4S6Gstatementcor, section 6.3hott_book
cardinal number, addition ofconceptindex, section C.2hott_book
function extensionality, proof from univalenceconceptindex, section 3.9hott_book
category, sliceconceptindex, section C.5hott_book
groupoid, higherconceptindex, section 1.1hott_book
XAX3KJ07GWstatementlem, section C.1.3hott_book
setconceptindex, section 3.6hott_book
judgmentconceptindex, section sec:formal-prelimhott_book
closed, termconceptindex, section 4.4hott_book
proposition, as typesconceptindex, section u1.u7hott_book
Lawvereconceptindex, section C.5hott_book
XDA9MZCPTGstatementcor, section C.5hott_book
$(\infty,1)$-topos, non-hypercompleteconceptindex, section 7.8hott_book
XE5XT4KQC1statementlem, section 5.4hott_book
XE7VXRVD87proofproof, section 9.11hott_book
completion, stackconceptindex, section 2.9hott_book
induction principle, for truncationconceptindex, section 6.3hott_book
prime numberconceptindex, section 9.10hott_book
category, center ofconceptindex, section 3.1hott_book
XFZ9B1DR9Kdefinitiondefn, section C.2hott_book
$n$-type, definable in type theoryconceptindex, section 9.11hott_book
XGRKENJA49proofproof, section 5.2hott_book
topological, spaceconceptindex, section 1hott_book
XHAYXEC42Sproofproof, section 6.5hott_book
Hopf Fibrationstatementthm, section 7.5hott_book
witness, to the truth of a propositionconceptindex, section A.1hott_book
sequence, fiberconceptindex, section 7.4hott_book
XK9P6M338Hstatementlem, section 2.4hott_book
XK9RPQ2FTWexerciseex, section 9.11hott_book
XKB26Y9TF6proofproof, section 2.5hott_book
XKK86CVRHSdefinitiondefn, section 9.3hott_book
mathematics, proof-relevantconceptindex, section 5.12hott_book
algebra, freeconceptindex, section 5.11hott_book
Cauchy, sequenceconceptindex, section Bhott_book
XMZF6QSETAdefinitiondefn, section 2.8hott_book
XN37SE0AYVstatementthm, section 1.11hott_book
whiskeringconceptindex, section 6.2hott_book
XPQTSTKVB1exerciseex, section 6.7hott_book
XPYD09V97Eproofproof, section 9.3hott_book
Lawvereconceptindex, section u1.u7hott_book
structural, set theoryconceptindex, section C.1.4hott_book
type, limitconceptindex, section 1.15hott_book
XR28YYFYG9exerciseex, section A.12.3hott_book
torusconceptindex, section 5.13hott_book
XR9QMK8G7Tproofproof, section 2.4hott_book
function, identityconceptindex, section 1.4hott_book
mathematics, classicalconceptindex, section 2.1hott_book
XRMVZN9S18proofproof, section 6.5hott_book
quantifier, existentialconceptindex, section 9.7hott_book
simplicial, kernelconceptindex, section 7.7.2hott_book
XS4BGHMWVBexampleeg, section 2.7hott_book
XSQ9GQVGZPproofproof, section 5.10hott_book
pushoutconceptindex, section 5.8hott_book
mathematics, constructiveconceptindex, section 7.10hott_book
XT94E70F2Zproofproof, section 1.6hott_book
XTGFRRA7WYstatementthm, section 6.1hott_book
$\infty$-groupoidconceptindex, section u1.u2hott_book
XV7WXS0PJHexerciseex, section B.6hott_book
retract, of a functionconceptindex, section 6.5hott_book
geometric realizationconceptindex, section 1hott_book
homotopy, typeconceptindex, section u1.u2hott_book
real numbers, agreeconceptindex, section B.4hott_book
implicit argumentconceptindex, section 4.2.11hott_book
XYGD5JK34Bexerciseex, section A.12.3hott_book
initial, $\sigma$-frameconceptindex, section B.4hott_book
identity, functionconceptindex, section 1.10hott_book
recursive callconceptindex, section A.9hott_book
monotonicityconceptindex, section B.3.2hott_book
Y0P3MF3572statementcor, section 7.4hott_book
function extensionalityconceptindex, section 1.15hott_book
formal, topologyconceptindex, section B.5hott_book
type, contractibleconceptindex, section 9.11hott_book
function, embeddingconceptindex, section 6.6hott_book
universal, property, of dependent pair typeconceptindex, section 1.15hott_book
first-order, logicconceptindex, section A.1hott_book
structure, identity principleconceptindex, section 2.8hott_book
isomorphism, semigroupconceptindex, section 1.14.2hott_book
mathematics, classicalconceptindex, section Bhott_book
loop, $n$-conceptindex, section 7.8hott_book
Y5ZKDJM6VTdefinitiondefn, section 2.3hott_book
\textsf{idtoiso}statementlem, section 2.1hott_book
function, retractionconceptindex, section 3.6hott_book
primitive, constantconceptindex, section 4.1hott_book
Y6T6NESYV1proofproof, section 3.1hott_book
cut, Dedekindconceptindex, section B.2.3hott_book
univalence axiomconceptindex, section 8.2hott_book
mathematics, constructiveconceptindex, section B.6hott_book
$(\infty,1)$-toposconceptindex, section u1.u8hott_book
presentation, of an $\infty$-groupoidconceptindex, section 5.1hott_book
mathematics, formalizedconceptindex, section u1.u8hott_book
Y9MQTVAKKWproofproof, section 7.5.3hott_book
YAD6JDCX58statementcor, section 6.3hott_book
YAGAWCS7ZGstatementlem, section 3.9hott_book
homologyconceptindex, section 7hott_book
pointwise, equality of functionsconceptindex, section 1.9hott_book
universal, property, of truncationconceptindex, section 5.9hott_book
coincidence, of Cauchy approximationsconceptindex, section B.3.2hott_book
type, $n$-sphereconceptindex, section 5.4hott_book
ringconceptindex, section B.2.1hott_book
YCA0Z1PN2Xdefinitiondefn, section 2.4hott_book
kernel, simplicialconceptindex, section 7.7.2hott_book
recursion, structuralconceptindex, section 4.1hott_book
spanconceptindex, section 5.9hott_book
mathematics, classicalconceptindex, section B.2hott_book
YFW4RYH1QNstatementthm, section 1.6hott_book
generation, of a type, inductiveconceptindex, section 5.1hott_book
YG5FEAZM6Ndefinitiondefn, section 3.2hott_book
YGE4QV00DFproofproof, section 6.5hott_book
decidable, equalityconceptindex, section 5.11hott_book
YH2PRVYV84proofproof, section 7.7.2hott_book
coherenceconceptindex, section 2.2hott_book
$\sigma$-frame, initialconceptindex, section B.2hott_book
setconceptindex, section 9.1hott_book
``continuity'' of functions in type theoryconceptindex, section 9.2hott_book
$(\infty,1)$-categoryconceptindex, section 1.15hott_book
induction principle, for cumulative hierarchyconceptindex, section C.5hott_book
YJX8XJ9VZNstatementthm, section B.3.2hott_book
YJY8A1YTRFexerciseex, section 5.13hott_book
group, abelianconceptindex, section 1.1hott_book
topological, spaceconceptindex, section 7hott_book
fundamental, groupoidconceptindex, section 2.9hott_book
YKZW0TKZCXstatementlem, section B.3.2hott_book
join, in a latticeconceptindex, section B.2hott_book
YMEK2855VEdefinitiondefn, section 6.1hott_book
homotopyconceptindex, section 1.4hott_book
YN4FGB199Edefinitiondefn, section 2.2hott_book
type, of vectorsconceptindex, section 8.7hott_book
adverbconceptindex, section 9.10hott_book
universal, property, of pushoutconceptindex, section 6.4hott_book
YPMJE8D9EFexerciseex, section 6.7hott_book
``continuity'' of functions in type theoryconceptindex, section 9.1hott_book
impredicative, quotientconceptindex, section 5.10hott_book
YQBX4K0F8Zstatementcor, section B.4hott_book
YQBY4BRPY1exerciseex, section 1.15hott_book
ordered field, archimedeanconceptindex, section B.3.3hott_book
mathematics, constructiveconceptindex, section Chott_book
setoidconceptindex, section C.1.4hott_book
denialconceptindex, section 9.8hott_book
YSR6DV01HTproofproof, section C.2hott_book
decidable, subsetconceptindex, section A.8hott_book
Proof of \cref{thm:freudcode}proofproof, section 7.6hott_book
YTMYMNDDGWexerciseex, section 3.9hott_book
fundamental, groupconceptindex, section 7.7.1hott_book
Lebesgue numberconceptindex, section B.5hott_book
algorithmconceptindex, section A.11hott_book
YXGGPNDG41exerciseex, section 3.9hott_book
YXJZYHY0PAdefinitiondefn, section 2.7hott_book
``functoriality'' of functions in type theoryconceptindex, section 9.2hott_book
$\w$-type, as homotopy-initial algebraconceptindex, section 8.4hott_book
implicationconceptindex, section A.11hott_book
YYGXNWB4SKproofproof, section C.4hott_book
derivationconceptindex, section 4.2hott_book
YYW2GM388Qstatementlem, section 7.6hott_book
YZ48QBP9RKstatementlem, section 2.7hott_book
YZ82TCW1Q8statementcor, section 6.5hott_book
type, dependent pairconceptindex, section 4.2.5hott_book
``continuity'' of functions in type theoryconceptindex, section 1.9hott_book
Covering spacesstatementthm, section 7.10hott_book
Sketch of proofproofproof, section 8.4hott_book
limit, of a Cauchy approximationconceptindex, section B.3.1hott_book
context, well-formedconceptindex, section sec:formal-prelimhott_book
stackconceptindex, section 2.9hott_book
Z3AD77MFFJstatementlem, section 3.7hott_book
predicate, inductiveconceptindex, section 8.7hott_book
$(\infty,1)$-toposconceptindex, section 3.8hott_book
scopeconceptindex, section sec:formal-prelimhott_book
Z47VA332WWproofproof, section 7.1.4hott_book
mathematics, constructiveconceptindex, section u1.u7hott_book
Z4TS0Z3WFGstatementlem, section 5.8hott_book
The principle of unique choicestatementcor, section 9.9hott_book
Z5CYSPDXDCproofproof, section 6.3hott_book
Hopf fibrationconceptindex, section 7.5.3hott_book
Z6XR8S0E49exerciseex, section C.5hott_book
Universal property of truncationsstatementlem, section 6.3hott_book
isomorphism, of setsconceptindex, section 1.4hott_book
quantifierconceptindex, section A.11hott_book
Z7GG3WEBNNexerciseex, section C.5hott_book
$\beta $-reductionconceptindex, section A.2hott_book
Z8TGBEDEK1exerciseex, section 5.13hott_book
depressionconceptindex, section B.4hott_book
caves, walls ofconceptindex, section 8.2hott_book
universal, property, of coproductconceptindex, section 1.15hott_book
Z9Q7BK0YHRstatementcor, section B.5hott_book
open, cutconceptindex, section B.2hott_book
logic, classical vs constructiveconceptindex, section A.11hott_book
univalence axiomconceptindex, section 8.8hott_book
ZBHB96M4RJdefinitiondefn, section 2.1hott_book
ZBRRFSSKVSexampleeg, section 2.1hott_book
associativity, in a groupconceptindex, section 5.11hott_book
ZD30J33V9Kstatementlem, section B.3.3hott_book
ZDZA52QMYZstatementthm, section 7.8hott_book
Second proofproofproof, section 1.3hott_book
mathematics, constructiveconceptindex, section B.3hott_book
mathematics, formalizedconceptindex, section u1.u1hott_book
structural, rulesconceptindex, section 4.2.2hott_book
topos, booleanconceptindex, section C.1.5hott_book
semiringconceptindex, section A.12.3hott_book
computation rule, for dependent function typesconceptindex, section A.4hott_book
Naive van Kampen theoremstatementthm, section 7.7.1hott_book
proof, assistant, Coqconceptindex, section 9.11hott_book
ZH4K8FS57Gstatementlem, section 5.4hott_book
quantifier, universalconceptindex, section 9.6hott_book
distanceconceptindex, section B.6hott_book
ZHAW7ZV17Dproofproof, section 6.2hott_book
ZHKYT44901statementthm, section 1.11hott_book
ZHVQMP6M9Hproofproof, section 8.8hott_book
ZHZ63AGWT9statementcor, section 7.8hott_book
diagramconceptindex, section 1.4hott_book
ZK9EYJ7CXAproofproof, section 2.5hott_book
substitutionconceptindex, section A.2hott_book
case analysisconceptindex, section 8.1hott_book
ZMBSPQYC1Fexerciseex, section B.6hott_book
normal formconceptindex, section 4.4hott_book
inductive-recursive typeconceptindex, section 8.7hott_book
double negation, law ofconceptindex, section 9.2hott_book
zeroconceptindex, section 8.1hott_book
logic, constructive vs classicalconceptindex, section 9.2hott_book
ZPKYKDNR47definitiondefn, section 2.2hott_book
Kan complexconceptindex, section u1.u2hott_book
Proof of~\cref{thm:omg}proofproof, section 1.1hott_book
ZPX90TY1EKexerciseex, section B.6hott_book
ZQ5JF1YYFPproofproof, section 9.3hott_book
ZQ7CAX7SB2exerciseex, section 3.9hott_book
open, problemconceptindex, section 1.15hott_book
inhabited typeconceptindex, section 9.4hott_book
initial, setconceptindex, section C.1.4hott_book
functor, contravariantconceptindex, section 8.6hott_book
$\sigma$-frame, initialconceptindex, section B.4hott_book
type, universeconceptindex, section 1.10hott_book
function, non-expandingconceptindex, section B.3.3hott_book
ZVV8H283XMexerciseex, section 2.9hott_book
ZW7JZYTPC5statementlem, section 2.2hott_book
fibration, of pathsconceptindex, section 7.1.2hott_book
inductive-inductive typeconceptindex, section 8.7hott_book
ZXF4V4PTD6proofproof, section 9.11hott_book
cardinal number, exponentiation ofconceptindex, section C.2hott_book
ZY7HDMYAGEproofproof, section 3.2hott_book
boolean, toposconceptindex, section C.1.5hott_book
hypothesis, homotopyconceptindex, section 1hott_book
attaching mapconceptindex, section 7.7.2hott_book

Catalogue records