main.labelnumbers.first-edition

\newlabel{analysis-bw-lpo}{11.5.9}
\newlabel{analysis-interval-ctb}{11.5.6}
\newlabel{axiom:funext}{2.9.3}
\newlabel{axiom:univalence}{2.10.3}
\newlabel{Blakers-Massey}{8.10.2}
\newlabel{card:exp}{10.2.6}
\newlabel{card:semiring}{10.2.4}
\newlabel{cha:basics}{2}
\newlabel{cha:category-theory}{9}
\newlabel{cha:equivalences}{4}
\newlabel{cha:hits}{6}
\newlabel{cha:hlevels}{7}
\newlabel{cha:homotopy}{8}
\newlabel{cha:induction}{5}
\newlabel{cha:logic}{3}
\newlabel{cha:preface}{}
\newlabel{cha:real-numbers}{11}
\newlabel{cha:rules}{A}
\newlabel{cha:set-math}{10}
\newlabel{cha:typetheory}{1}
\newlabel{classical-Heine-Borel}{11.5.11}
\newlabel{connectedtotruncated}{7.5.9}
\newlabel{contrfamtotalpostcompequiv}{4.9.3}
\newlabel{cor:Delta0sep}{10.5.9}
\newlabel{cor:freudenthal-equiv}{8.6.14}
\newlabel{cor:hom-fg}{2.4.4}
\newlabel{cor:omega-s1}{8.1.10}
\newlabel{cor:pi1s1}{8.1.11}
\newlabel{cor:pis2-hopf}{8.5.2}
\newlabel{cor:preservation-hlevels-weq}{7.1.5}
\newlabel{cor:sn-connected}{8.2.2}
\newlabel{cor:stability-spheres}{8.6.15}
\newlabel{cor:totrunc-is-connected}{7.5.8}
\newlabel{cor:transport-path-prepost}{2.11.2}
\newlabel{cor:trunc-prod}{7.3.8}
\newlabel{cor:trunc_prod}{7.7.3}
\newlabel{cor:UC}{3.9.2}
\newlabel{cref@analysis-bw-lpo}{[thm][9][11,5]11.5.9}
\newlabel{cref@analysis-interval-ctb}{[thm][6][11,5]11.5.6}
\newlabel{cref@axiom:funext}{[axiom][3][2,9]2.9.3}
\newlabel{cref@axiom:univalence}{[axiom][3][2,10]2.10.3}
\newlabel{cref@Blakers-Massey}{[thm][2][8,10]8.10.2}
\newlabel{cref@card:exp}{[lem][6][10,2]10.2.6}
\newlabel{cref@card:semiring}{[lem][4][10,2]10.2.4}
\newlabel{cref@cha:basics}{[chapter][2][]2}
\newlabel{cref@cha:category-theory}{[chapter][9][]9}
\newlabel{cref@cha:equivalences}{[chapter][4][]4}
\newlabel{cref@cha:hits}{[chapter][6][]6}
\newlabel{cref@cha:hlevels}{[chapter][7][]7}
\newlabel{cref@cha:homotopy}{[chapter][8][]8}
\newlabel{cref@cha:induction}{[chapter][5][]5}
\newlabel{cref@cha:logic}{[chapter][3][]3}
\newlabel{cref@cha:preface}{}
\newlabel{cref@cha:real-numbers}{[chapter][11][]11}
\newlabel{cref@cha:rules}{[appendix][1][2147483647]A}
\newlabel{cref@cha:set-math}{[chapter][10][]10}
\newlabel{cref@cha:typetheory}{[chapter][1][]1}
\newlabel{cref@classical-Heine-Borel}{[thm][11][11,5]11.5.11}
\newlabel{cref@connectedtotruncated}{[cor][9][7,5]7.5.9}
\newlabel{cref@contrfamtotalpostcompequiv}{[cor][3][4,9]4.9.3}
\newlabel{cref@cor:Delta0sep}{[cor][9][10,5]10.5.9}
\newlabel{cref@cor:freudenthal-equiv}{[cor][14][8,6]8.6.14}
\newlabel{cref@cor:hom-fg}{[cor][4][2,4]2.4.4}
\newlabel{cref@cor:omega-s1}{[cor][10][8,1]8.1.10}
\newlabel{cref@cor:pi1s1}{[cor][11][8,1]8.1.11}
\newlabel{cref@cor:pis2-hopf}{[cor][2][8,5]8.5.2}
\newlabel{cref@cor:preservation-hlevels-weq}{[cor][5][7,1]7.1.5}
\newlabel{cref@cor:sn-connected}{[cor][2][8,2]8.2.2}
\newlabel{cref@cor:stability-spheres}{[cor][15][8,6]8.6.15}
\newlabel{cref@cor:totrunc-is-connected}{[cor][8][7,5]7.5.8}
\newlabel{cref@cor:transport-path-prepost}{[lem][2][2,11]2.11.2}
\newlabel{cref@cor:trunc_prod}{[cor][3][7,7]7.7.3}
\newlabel{cref@cor:trunc-prod}{[thm][8][7,3]7.3.8}
\newlabel{cref@cor:UC}{[cor][2][3,9]3.9.2}
\newlabel{cref@ct:2cat}{[ex][5][9]9.5}
\newlabel{cref@ct:adjointification}{[lem][2][9,4]9.4.2}
\newlabel{cref@ct:adjprop2}{[cor][11][9,5]9.5.11}
\newlabel{cref@ct:adjprop}{[lem][2][9,3]9.3.2}
\newlabel{cref@ct:adj-repr}{[lem][10][9,5]9.5.10}
\newlabel{cref@ctb-uniformly-continuous-sup}{[thm][7][11,5]11.5.7}
\newlabel{cref@ct:cat-2cat}{[thm][16][9,4]9.4.16}
\newlabel{cref@ct:category}{[defn][6][9,1]9.1.6}
\newlabel{cref@ct:cat-eq-iso}{[lem][15][9,4]9.4.15}
\newlabel{cref@ct:cat-weq-eq}{[thm][4][9,9]9.9.4}
\newlabel{cref@ct:catweq}{[lem][7][9,4]9.4.7}
\newlabel{cref@ct:chaotic}{[eg][13][9,4]9.4.13}
\newlabel{cref@ct:discrete}{[eg][16][9,1]9.1.16}
\newlabel{cref@ct:eg:set}{[eg][7][9,1]9.1.7}
\newlabel{cref@ct:equiv}{[defn][1][9,4]9.4.1}
\newlabel{cref@ct:eqv-levelwise}{[lem][14][9,4]9.4.14}
\newlabel{cref@ct:esofull-precomp-ff}{[lem][2][9,9]9.9.2}
\newlabel{cref@ct:ex:hocat}{[ex][9][9]9.9}
\newlabel{cref@ct:ffeso}{[lem][5][9,4]9.4.5}
\newlabel{cref@ct:functor-assoc}{[lem][9][9,2]9.2.9}
\newlabel{cref@ct:functor-cat}{[thm][5][9,2]9.2.5}
\newlabel{cref@ct:functor}{[defn][1][9,2]9.2.1}
\newlabel{cref@ct:functorexpadj}{[lem][3][9,5]9.5.3}
\newlabel{cref@ct:functor-precat}{[defn][3][9,2]9.2.3}
\newlabel{cref@ct:fundgpd}{[eg][17][9,1]9.1.17}
\newlabel{cref@ct:galois}{[eg][3][9,6]9.6.3}
\newlabel{cref@ct:gaunt}{[eg][15][9,1]9.1.15}
\newlabel{cref@ct:groupoids}{[ex][6][9]9.6}
\newlabel{cref@ct:hilb}{[eg][7][9,7]9.7.7}
\newlabel{cref@ct:hocat}{[eg][7][9,9]9.9.7}
\newlabel{cref@ct:hoprecat}{[eg][18][9,1]9.1.18}
\newlabel{cref@ct:idtoisocompute}{[equation][10][9,1]9.1.10}
\newlabel{cref@ct:idtoiso}{[lem][4][9,1]9.1.4}
\newlabel{cref@ct:idtoiso-trans}{[lem][9][9,1]9.1.9}
\newlabel{cref@ct:idtounitary}{[lem][3][9,7]9.7.3}
\newlabel{cref@ct:interchange}{[lem][8][9,2]9.2.8}
\newlabel{cref@ct:isocat}{[defn][8][9,4]9.4.8}
\newlabel{cref@ct:isomorphism}{[defn][2][9,1]9.1.2}
\newlabel{cref@ct:isoprecat}{[lem][9][9,4]9.4.9}
\newlabel{cref@ct:isoprop}{[lem][3][9,1]9.1.3}
\newlabel{cref@ct:natiso}{[lem][4][9,2]9.2.4}
\newlabel{cref@ct:nattrans}{[defn][2][9,2]9.2.2}
\newlabel{cref@ct:obj-1type}{[lem][8][9,1]9.1.8}
\newlabel{cref@ct:opposite-category}{[defn][1][9,5]9.5.1}
\newlabel{cref@ct:orders}{[eg][14][9,1]9.1.14}
\newlabel{cref@ct:pentagon}{[lem][10][9,2]9.2.10}
\newlabel{cref@ct:pre2cat}{[ex][4][9]9.4}
\newlabel{cref@ct:precategory}{[defn][1][9,1]9.1.1}
\newlabel{cref@ct:precatset}{[eg][5][9,1]9.1.5}
\newlabel{cref@ct:rel}{[eg][19][9,1]9.1.19}
\newlabel{cref@ct:representable}{[defn][8][9,5]9.5.8}
\newlabel{cref@ct:representable-prop}{[thm][9][9,5]9.5.9}
\newlabel{cref@ct:rezk-fundgpd-trunc1}{[eg][6][9,9]9.9.6}
\newlabel{cref@ct:sig}{[defn][1][9,8]9.8.1}
\newlabel{cref@ct:sip-functor-cat}{[eg][3][9,8]9.8.3}
\newlabel{cref@ct:unitary}{[defn][2][9,7]9.7.2}
\newlabel{cref@ct:units}{[lem][11][9,2]9.2.11}
\newlabel{cref@ct:yoneda-embedding}{[cor][6][9,5]9.5.6}
\newlabel{cref@ct:yoneda-mono}{[cor][7][9,5]9.5.7}
\newlabel{cref@ct:yoneda}{[thm][4][9,5]9.5.4}
\newlabel{cref@dedekind-in-cut-as-le}{[lem][2][11,2]11.2.2}
\newlabel{cref@def:bisimulation}{[defn][4][10,5]10.5.4}
\newlabel{cref@def:hlevel}{[defn][1][7,1]7.1.1}
\newlabel{cref@def:loopspace}{[defn][8][2,1]2.1.8}
\newlabel{cref@defn:1type}{[defn][7][3,1]3.1.7}
\newlabel{cref@defn:accessibility}{[defn][1][10,3]10.3.1}
\newlabel{cref@defn:biinv}{[defn][1][4,3]4.3.1}
\newlabel{cref@defn:card}{[defn][1][10,2]10.2.1}
\newlabel{cref@defn:cauchy-approximation}{[defn][10][11,2]11.2.10}
\newlabel{cref@defn:cauchy-reals}{[defn][2][11,3]11.3.2}
\newlabel{cref@defn:cocone}{[defn][1][6,8]6.8.1}
\newlabel{cref@defn:complete-metric-space}{[defn][2][11,5]11.5.2}
\newlabel{cref@defn:contractible}{[defn][1][3,11]3.11.1}
\newlabel{cref@defn:decidable-equality}{[defn][3][3,4]3.4.3}
\newlabel{cref@defn:dedekind-reals}{[defn][1][11,2]11.2.1}
\newlabel{cref@defn:equivalence}{[defn][1][4,4]4.4.1}
\newlabel{cref@defn:fo-notion-of-structure}{[defn][4][9,8]9.8.4}
\newlabel{cref@defn:homotopy}{[defn][1][2,4]2.4.1}
\newlabel{cref@defn:homotopy-fiber}{[defn][4][4,2]4.2.4}
\newlabel{cref@defn:identity-systems}{[defn][1][5,8]5.8.1}
\newlabel{cref@defn:inductive-cover}{[defn][13][11,5]11.5.13}
\newlabel{cref@defn:inductive-cover-interval-1}{[enumi][5][](v)}
\newlabel{cref@defn:inductive-cover-interval-2}{[enumi][6][](vi)}
\newlabel{cref@defn:ishae}{[defn][1][4,2]4.2.1}
\newlabel{cref@defn:isprop}{[defn][1][3,3]3.3.1}
\newlabel{cref@defn:lcoh-rcoh}{[defn][10][4,2]4.2.10}
\newlabel{cref@defn:linv-rinv}{[defn][7][4,2]4.2.7}
\newlabel{cref@defn:lipschitz}{[defn][14][11,3]11.3.14}
\newlabel{cref@defn:logical-notation}{[defn][1][3,7]3.7.1}
\newlabel{cref@defn:metric-space}{[defn][1][11,5]11.5.1}
\newlabel{cref@defn:modal-image}{[defn][3][7,6]7.6.3}
\newlabel{cref@defn:modality}{[defn][5][7,7]7.7.5}
\newlabel{cref@defn:nalg}{[defn][1][5,4]5.4.1}
\newlabel{cref@defn:nhom}{[defn][2][5,4]5.4.2}
\newlabel{cref@defn:No-codes}{[thm][7][11,6]11.6.7}
\newlabel{cref@defn:RC-approx}{[thm][16][11,3]11.3.16}
\newlabel{cref@defn:reflective-subuniverse}{[defn][1][7,7]7.7.1}
\newlabel{cref@defn:retract}{[defn][2][4,7]4.7.2}
\newlabel{cref@defn:set}{[defn][1][3,1]3.1.1}
\newlabel{cref@defn:setof}{[lem][1][3,5]3.5.1}
\newlabel{cref@defn:surreals}{[defn][1][11,6]11.6.1}
\newlabel{cref@defn:total-bounded-metric-space}{[defn][3][11,5]11.5.3}
\newlabel{cref@defn:total-map}{[defn][5][4,7]4.7.5}
\newlabel{cref@defn:uniformly-continuous}{[defn][5][11,5]11.5.5}
\newlabel{cref@defn:V}{[defn][1][10,5]10.5.1}
\newlabel{cref@defn-Z}{[rmk][7][6,10]6.10.7}
\newlabel{cref@def-of-homotopy-groups}{[defn][1][8,0]8.0.1}
\newlabel{cref@def:pointedmap}{[defn][1][8,4]8.4.1}
\newlabel{cref@def:pointedtype}{[defn][7][2,1]2.1.7}
\newlabel{cref@def:simulation}{[defn][11][10,3]10.3.11}
\newlabel{cref@def:TypeOfElements}{[defn][7][10,5]10.5.7}
\newlabel{cref@def:VVquotient}{[defn][5][6,10]6.10.5}
\newlabel{cref@eg:circle}{[eg][6][8,7]8.7.6}
\newlabel{cref@eg:clvk}{[eg][13][8,7]8.7.13}
\newlabel{cref@eg:cofiber}{[eg][14][8,7]8.7.14}
\newlabel{cref@eg:concatequiv}{[eg][8][2,4]2.4.8}
\newlabel{cref@eg:idequiv}{[eg][7][2,4]2.4.7}
\newlabel{cref@eg:kg1}{[eg][17][8,7]8.7.17}
\newlabel{cref@eg:suspension}{[eg][7][8,7]8.7.7}
\newlabel{cref@eg:torus}{[eg][15][8,7]8.7.15}
\newlabel{cref@eg:unnatural-hit}{[eg][1][6,13]6.13.1}
\newlabel{cref@eg:wedge}{[eg][8][8,7]8.7.8}
\newlabel{cref@Eilenberg-Mac-Lane-Spaces}{[thm][3][8,10]8.10.3}
\newlabel{cref@epis-surj}{[lem][4][10,1]10.1.4}
\newlabel{cref@eq:ac}{[equation][1][3,8]3.8.1}
\newlabel{cref@eq:apd-to-ap}{[equation][7][2,3]2.3.7}
\newlabel{cref@eq:appxrec2}{[equation][24][11,3]11.3.24}
\newlabel{cref@eq:ap-to-apd}{[equation][6][2,3]2.3.6}
\newlabel{cref@eq:bfa-bga2}{[equation][11][8,7]8.7.11}
\newlabel{cref@eq:bfa-bga-comm}{[equation][2][8,7]8.7.2}
\newlabel{cref@eq:bfa-bga}{[equation][1][8,7]8.7.1}
\newlabel{cref@eq:cauchy-approx}{[equation][11][11,2]11.2.11}
\newlabel{cref@eq:cauchy-sequence}{[equation][9][11,2]11.2.9}
\newlabel{cref@eq:class-notation}{[equation][3][10,5]10.5.3}
\newlabel{cref@eq:composeconefunc}{[equation][4][7,4]7.4.4}
\newlabel{cref@eq:composeconeid}{[equation][3][7,4]7.4.3}
\newlabel{cref@eq:concatD}{[equation][3][2,1]2.1.3}
\newlabel{cref@eq:conetrunc}{[equation][11][7,4]7.4.11}
\newlabel{cref@eq:cover-pointwise}{[equation][12][11,5]11.5.12}
\newlabel{cref@eq:cover-pointwise-truncated}{[equation][10][11,5]11.5.10}
\newlabel{cref@eq:ct:gbar}{[equation][12][9,4]9.4.12}
\newlabel{cref@eq:ct:ipctri}{[equation][11][9,4]9.4.11}
\newlabel{cref@eq:ct:isoprecattri}{[equation][10][9,4]9.4.10}
\newlabel{cref@eq:dbl0}{[equation][1][1,10]1.10.1}
\newlabel{cref@eq:dbl-as-rec}{[equation][1][1,9]1.9.1}
\newlabel{cref@eq:dblsuc}{[equation][2][1,10]1.10.2}
\newlabel{cref@eq:decode}{[equation][5][8,7]8.7.5}
\newlabel{cref@eq:defn-pullback}{[equation][11][2,15]2.15.11}
\newlabel{cref@eq:depCauchyappx}{[equation][5][11,3]11.3.5}
\newlabel{cref@eq:dnshift}{[equation][11][3,11]3.11.11}
\newlabel{cref@eq:dpath}{[equation][2][6,2]6.2.2}
\newlabel{cref@eq:english-ac}{[equation][1][3,2]3.2.1}
\newlabel{cref@eq:epis-split}{[equation][3][3,8]3.8.3}
\newlabel{cref@eq:equality-semigroup-mult}{[subsection][2][]2.14.2}
\newlabel{cref@eq:eqv}{[equation][11][2,4]2.4.11}
\newlabel{cref@eq:example-comp}{[equation][6][5,6]5.6.6}
\newlabel{cref@eq:example-constructor}{[equation][4][5,6]5.6.4}
\newlabel{cref@eq:example-indhyp}{[equation][7][5,6]5.6.7}
\newlabel{cref@eq:example-rechyp}{[equation][5][5,6]5.6.5}
\newlabel{cref@eq:expldef}{[equation][1][1,2]1.2.1}
\newlabel{cref@eq:fake-recursor}{[equation][1][5,6]5.6.1}
\newlabel{cref@eq:ffprime-north}{[equation][5][6,5]6.5.5}
\newlabel{cref@eq:flattening-rectnd}{[equation][6][6,12]6.12.6}
\newlabel{cref@eq:fpaut}{[equation][3][3,2]3.2.3}
\newlabel{cref@eq:fpfaut}{[equation][4][3,2]3.2.4}
\newlabel{cref@eq:freudcode}{[equation][6][8,6]8.6.6}
\newlabel{cref@eq:freudcodeN}{[equation][7][8,6]8.6.7}
\newlabel{cref@eq:freudcodeS}{[equation][8][8,6]8.6.8}
\newlabel{cref@eq:freudcompute1}{[equation][11][8,6]8.6.11}
\newlabel{cref@eq:freudcompute2}{[equation][12][8,6]8.6.12}
\newlabel{cref@eq:freudenthal-for-spheres}{[equation][16][8,6]8.6.16}
\newlabel{cref@eq:freudgoal}{[equation][13][8,6]8.6.13}
\newlabel{cref@eq:freudmap}{[equation][9][8,6]8.6.9}
\newlabel{cref@eq:fullprop}{[equation][3][9,9]9.9.3}
\newlabel{cref@eq:happly}{[equation][2][2,9]2.9.2}
\newlabel{cref@eq:injective}{[equation][2][4,6]4.6.2}
\newlabel{cref@eq:inlinj}{[equation][1][2,12]2.12.1}
\newlabel{cref@eq:inlrdj}{[equation][3][2,12]2.12.3}
\newlabel{cref@eq:iscontrf}{[equation][2][4,4]4.4.2}
\newlabel{cref@eq:isequiv-invertible}{[equation][10][2,4]2.4.10}
\newlabel{cref@eq:Jconv}{[equation][1][2,0]2.0.1}
\newlabel{cref@eq:lambda-abstraction}{[equation][1][1,4]1.4.1}
\newlabel{cref@eq:ldn}{[equation][2][3,4]3.4.2}
\newlabel{cref@eq:lem}{[equation][1][3,4]3.4.1}
\newlabel{cref@eq:lpo}{[equation][8][11,5]11.5.8}
\newlabel{cref@eq:mapofspans-htpy}{[equation][9][7,4]7.4.9}
\newlabel{cref@eq:modaltype}{[equation][6][7,7]7.7.6}
\newlabel{cref@eq:NO-codes-transitivity}{[equation][9][11,6]11.6.9}
\newlabel{cref@eq:NO-codes-unstrict}{[equation][8][11,6]11.6.8}
\newlabel{cref@eq:noind1}{[equation][3][11,6]11.6.3}
\newlabel{cref@eq:NO-prec-def}{[equation][15][11,6]11.6.15}
\newlabel{cref@eq:NO-preceq-def}{[equation][14][11,6]11.6.14}
\newlabel{cref@eq:NO-prec-IHL}{[equation][12][11,6]11.6.12}
\newlabel{cref@eq:NO-prec-IHR}{[equation][13][11,6]11.6.13}
\newlabel{cref@eq:NO-prec-outer-IH}{[equation][10][11,6]11.6.10}
\newlabel{cref@eq:path-forall}{[equation][1][2,9]2.9.1}
\newlabel{cref@eq:path-lump}{[equation][10][2,15]2.15.10}
\newlabel{cref@eq:path-prod}{[equation][1][2,6]2.6.1}
\newlabel{cref@eq:path-prod-inverse}{[equation][3][2,6]2.6.3}
\newlabel{cref@eq:path-trunc-map}{[equation][11][7,3]7.3.11}
\newlabel{cref@eq:pi1s1-decode}{[equation][4][8,1]8.1.4}
\newlabel{cref@eq:pi1s1-encode}{[equation][3][8,1]8.1.3}
\newlabel{cref@eq:Pinj}{[equation][2][5,6]5.6.2}
\newlabel{cref@eq:polyfunc}{[equation][6][5,4]5.4.6}
\newlabel{cref@eq:prodeqv}{[equation][1][2,5]2.5.1}
\newlabel{cref@eq:prod-umpd-map}{[equation][4][2,15]2.15.4}
\newlabel{cref@eq:prod-ump-map}{[equation][1][2,15]2.15.1}
\newlabel{cref@eq:prod-ump-rt1}{[equation][3][2,15]2.15.3}
\newlabel{cref@eq:prod-ump-rt2}{[equation][8][2,15]2.15.8}
\newlabel{cref@eq:prop-up}{[equation][4][3,5]3.5.4}
\newlabel{cref@eq:qinvtype}{[equation][5][2,4]2.4.5}
\newlabel{cref@eq:quotient-when-canonical}{[equation][9][6,10]6.10.9}
\newlabel{cref@eq:RCappx1}{[equation][17][11,3]11.3.17}
\newlabel{cref@eq:RCappx2}{[equation][18][11,3]11.3.18}
\newlabel{cref@eq:RCappx3}{[equation][19][11,3]11.3.19}
\newlabel{cref@eq:RCappx4}{[equation][20][11,3]11.3.20}
\newlabel{cref@eq:RCappx-rtri-rll1}{[equation][29][11,3]11.3.29}
\newlabel{cref@eq:RCappx-rtri-rll2}{[equation][30][11,3]11.3.30}
\newlabel{cref@eq:RCappx-rtri-rll3}{[equation][31][11,3]11.3.31}
\newlabel{cref@eq:RCappx-rtri-rlr1}{[equation][27][11,3]11.3.27}
\newlabel{cref@eq:RCappx-rtri-rlr2}{[equation][28][11,3]11.3.28}
\newlabel{cref@eq:RCappx-rtri-rrl1}{[equation][25][11,3]11.3.25}
\newlabel{cref@eq:RCappx-rtri-rrl2}{[equation][26][11,3]11.3.26}
\newlabel{cref@eq:RC-cauchy}{[equation][3][11,3]11.3.3}
\newlabel{cref@eq:RC-path}{[equation][4][11,3]11.3.4}
\newlabel{cref@eq:rcsimind1}{[equation][6][11,3]11.3.6}
\newlabel{cref@eq:rcsimind2}{[equation][7][11,3]11.3.7}
\newlabel{cref@eq:RC-sim-ltri}{[equation][23][11,3]11.3.23}
\newlabel{cref@eq:RC-sim-recursion-extra}{[equation][13][11,3]11.3.13}
\newlabel{cref@eq:RC-sim-rtri}{[equation][22][11,3]11.3.22}
\newlabel{cref@eq:RD-linear-order}{[equation][3][11,2]11.2.3}
\newlabel{cref@eq:S1recindbase}{[equation][6][6,2]6.2.6}
\newlabel{cref@eq:S1recindloop}{[equation][7][6,2]6.2.7}
\newlabel{cref@eq:set-up}{[equation][3][3,5]3.5.3}
\newlabel{cref@eq:sigma-lump}{[equation][9][2,15]2.15.9}
\newlabel{cref@eq:sigma-ump-map}{[equation][6][2,15]2.15.6}
\newlabel{cref@eq:Snsusp}{[equation][2][6,5]6.5.2}
\newlabel{cref@eq:subset}{[equation][2][3,5]3.5.2}
\newlabel{cref@eq:suc-injective}{[equation][3][2,13]2.13.3}
\newlabel{cref@eq:sumcodefam}{[equation][4][2,12]2.12.4}
\newlabel{cref@eq:tautology1}{[equation][1][1,11]1.11.1}
\newlabel{cref@eq:tautology2}{[equation][2][1,11]1.11.2}
\newlabel{cref@eq:transport-arrow}{[equation][4][2,9]2.9.4}
\newlabel{cref@eq:transport-arrow-families}{[equation][5][2,9]2.9.5}
\newlabel{cref@eq:transport-semigroup-assoc}{[equation][3][2,14]2.14.3}
\newlabel{cref@eq:transport-semigroup-step1}{[equation][2][2,14]2.14.2}
\newlabel{cref@eq:trunc-htpy}{[equation][6][7,3]7.3.6}
\newlabel{cref@eq:trunc-nat}{[equation][4][7,3]7.3.4}
\newlabel{cref@eq:uatofeps}{[equation][7][4,9]4.9.7}
\newlabel{cref@eq:uatofesp}{[equation][6][4,9]4.9.6}
\newlabel{cref@eq:uidtoeqv}{[equation][2][2,10]2.10.2}
\newlabel{cref@eq:untruncated-linearity}{[equation][2][11,4]11.4.2}
\newlabel{cref@equ:prequired}{[equation][8][5,4]5.4.8}
\newlabel{cref@eq:V-path}{[equation][2][10,5]10.5.2}
\newlabel{cref@eq:yoneda}{[equation][5][9,5]9.5.5}
\newlabel{cref@eq:zero-not-succ}{[equation][2][2,13]2.13.2}
\newlabel{cref@ex:acconn}{[ex][10][7]7.10}
\newlabel{cref@ex:ackermann}{[ex][10][1]1.10}
\newlabel{cref@ex:acnm}{[ex][8][7]7.8}
\newlabel{cref@ex:acnm-surjset}{[ex][9][7]7.9}
\newlabel{cref@ex:ap-path-inversion}{[ex][6][8]8.6}
\newlabel{cref@ex:ap-sigma}{[ex][7][2]2.7}
\newlabel{cref@ex:basics:concat}{[ex][1][2]2.1}
\newlabel{cref@ex:bool}{[ex][4][5]5.4}
\newlabel{cref@ex:brck-qinv}{[ex][8][3]3.8}
\newlabel{cref@ex:choice-function}{[ex][10][10]10.10}
\newlabel{cref@ex:composition}{[ex][1][1]1.1}
\newlabel{cref@ex:connectivity-inductively}{[ex][6][7]7.6}
\newlabel{cref@ex:coprod-ump}{[ex][9][2]2.9}
\newlabel{cref@ex:cumhierhit}{[ex][11][10]10.11}
\newlabel{cref@ex:decidable-choice}{[ex][19][3]3.19}
\newlabel{cref@ex:disjoint-or}{[ex][7][3]3.7}
\newlabel{cref@ex:equality-reflection}{[ex][14][2]2.14}
\newlabel{cref@ex:equiv-concat}{[ex][6][2]2.6}
\newlabel{cref@ex:eqvboolbool}{[ex][13][2]2.13}
\newlabel{cref@ex:fin}{[ex][9][1]1.9}
\newlabel{cref@ex:finite-cover-lebesgue-number}{[ex][12][11]11.12}
\newlabel{cref@ex:free-monoid}{[ex][8][6]6.8}
\newlabel{cref@ex:HopfJr}{[ex][8][8]8.8}
\newlabel{cref@ex:impred-brck}{[ex][15][3]3.15}
\newlabel{cref@ex:isset-coprod}{[ex][2][3]3.2}
\newlabel{cref@ex:isset-sigma}{[ex][3][3]3.3}
\newlabel{cref@ex:lem-brck}{[ex][14][3]3.14}
\newlabel{cref@ex:lem-impred}{[ex][10][3]3.10}
\newlabel{cref@ex:lem-ldn}{[ex][18][3]3.18}
\newlabel{cref@ex:lem-mereprop}{[ex][6][3]3.6}
\newlabel{cref@ex:lemnm}{[ex][7][7]7.7}
\newlabel{cref@ex:loop2}{[ex][8][5]5.8}
\newlabel{cref@ex:loop}{[ex][7][5]5.7}
\newlabel{cref@ex:mean-value-theorem}{[ex][13][11]11.13}
\newlabel{cref@ex:metric-completion}{[ex][9][11]11.9}
\newlabel{cref@ex:neg-ldn}{[ex][11][1]1.11}
\newlabel{cref@ex:ninf-ord}{[ex][8][10]10.8}
\newlabel{cref@ex:not-not-lem}{[ex][13][1]1.13}
\newlabel{cref@ex:npaths}{[ex][4][2]2.4}
\newlabel{cref@ex:nspheres}{[ex][4][6]6.4}
\newlabel{cref@ex:ntype-from-nconn-const}{[ex][5][7]7.5}
\newlabel{cref@ex:ntypes-closed-under-wtypes}{[ex][3][7]7.3}
\newlabel{cref@ex:omit-contr2}{[ex][20][3]3.20}
\newlabel{cref@ex:one-function-two-recurrences}{[ex][3][5]5.3}
\newlabel{cref@ex:pm-to-ml}{[ex][7][1]1.7}
\newlabel{cref@ex:pointed-equivalences}{[ex][7][8]8.7}
\newlabel{cref@ex:prod-via-bool}{[ex][6][1]1.6}
\newlabel{cref@ex:prop-endocontr}{[ex][4][3]3.4}
\newlabel{cref@ex:prop-inhabcontr}{[ex][5][3]3.5}
\newlabel{cref@ex:prop-ord}{[ex][7][10]10.7}
\newlabel{cref@ex:prop-trunc-ind}{[ex][17][3]3.17}
\newlabel{cref@ex:pullback}{[ex][11][2]2.11}
\newlabel{cref@ex:pullback-pasting}{[ex][12][2]2.12}
\newlabel{cref@ex:qinv-autohtpy-no-univalence}{[ex][3][4]4.3}
\newlabel{cref@ex:RD-extended-reals}{[ex][2][11]11.2}
\newlabel{cref@ex:RD-interval-arithmetic}{[ex][4][11]11.4}
\newlabel{cref@ex:RD-lower-cuts}{[ex][3][11]11.3}
\newlabel{cref@ex:RD-lt-vs-le}{[ex][5][11]11.5}
\newlabel{cref@ex:reals-apart-neq-MP}{[ex][10][11]11.10}
\newlabel{cref@ex:reals-apart-zero-divisors}{[ex][11][11]11.11}
\newlabel{cref@ex:reals-non-constant-into-Z}{[ex][6][11]11.6}
\newlabel{cref@ex:rezk-vankampen}{[ex][11][9]9.11}
\newlabel{cref@ex:s2-colim-unit}{[ex][2][7]7.2}
\newlabel{cref@ex:same-recurrence-not-defeq}{[ex][2][5]5.2}
\newlabel{cref@ex:sigma-assoc}{[ex][10][2]2.10}
\newlabel{cref@ex:stack}{[ex][12][9]9.12}
\newlabel{cref@ex:subtFromPathInd}{[ex][15][1]1.15}
\newlabel{cref@ex:sum-via-bool}{[ex][5][1]1.5}
\newlabel{cref@ex:SuperHopf}{[ex][9][8]8.9}
\newlabel{cref@ex:suspS1}{[ex][2][6]6.2}
\newlabel{cref@ex:tautologies}{[ex][12][1]1.12}
\newlabel{cref@ex:torus}{[ex][1][6]6.1}
\newlabel{cref@ex:torus-s1-times-s1}{[ex][3][6]6.3}
\newlabel{cref@ex:traditional-archimedean}{[ex][7][11]11.7}
\newlabel{cref@ex:unique-fiber}{[ex][5][8]8.5}
\newlabel{cref@ex:unnatural-endomorphisms}{[ex][9][6]6.9}
\newlabel{cref@ex:unstable-octahedron}{[ex][4][4]4.4}
\newlabel{cref@ex:vksuspnopt}{[ex][11][8]8.11}
\newlabel{cref@ex:vksusppt}{[ex][10][8]8.10}
\newlabel{cref@ex:well-pointed}{[ex][3][10]10.3}
\newlabel{cref@ex:without-K}{[ex][14][1]1.14}
\newlabel{cref@fibwise-fiber-total-fiber-equiv}{[thm][6][4,7]4.7.6}
\newlabel{cref@fig:hub-and-spokes}{[figure][3][6]6.3}
\newlabel{cref@fig:spokes-no-hub}{[figure][4][6]6.4}
\newlabel{cref@fig:spokes-no-hub-ii}{[figure][5][6]6.5}
\newlabel{cref@fig:topS1ind}{[figure][1][6]6.1}
\newlabel{cref@fig:ttS1ind}{[figure][2][6]6.2}
\newlabel{cref@fig:winding}{[figure][1][8]8.1}
\newlabel{cref@inductive-cover-classical}{[thm][16][11,5]11.5.16}
\newlabel{cref@interval-Heine-Borel}{[cor][15][11,5]11.5.15}
\newlabel{cref@item:apfunctor-compose}{[enumi][3][](iii)}
\newlabel{cref@item:apfunctor-ct}{[enumi][1][](i)}
\newlabel{cref@item:apfunctor-opp}{[enumi][2][](ii)}
\newlabel{cref@item:autohtpy1}{[enumi][1][](i)}
\newlabel{cref@item:autohtpy2}{[enumi][2][](ii)}
\newlabel{cref@item:autohtpy3}{[enumi][3][](iii)}
\newlabel{cref@item:be1}{[enumi][1][](i)}
\newlabel{cref@item:be2}{[enumi][2][](ii)}
\newlabel{cref@item:be3}{[enumi][3][](iii)}
\newlabel{cref@item:beb1}{[enumi][1][](i)}
\newlabel{cref@item:beb2}{[enumi][2][](ii)}
\newlabel{cref@item:beb3}{[enumi][3][](iii)}
\newlabel{cref@item:cle-inj}{[enumi][1][](i)}
\newlabel{cref@item:cle-surj}{[enumi][2][](ii)}
\newlabel{cref@item:conntest1}{[enumi][1][](i)}
\newlabel{cref@item:conntest2}{[enumi][2][](ii)}
\newlabel{cref@item:conntest3}{[enumi][3][](iii)}
\newlabel{cref@item:contr}{[enumi][1][](i)}
\newlabel{cref@item:contr-eqv-unit}{[enumi][3][](iii)}
\newlabel{cref@item:contr-inhabited-prop}{[enumi][2][](ii)}
\newlabel{cref@item:conway1}{[enumi][1][](i)}
\newlabel{cref@item:conway2}{[enumi][2][](ii)}
\newlabel{cref@item:ct:ar1}{[enumi][1][](i)}
\newlabel{cref@item:ct:ar2}{[enumi][2][](ii)}
\newlabel{cref@item:ct:ffeso1}{[enumi][1][](i)}
\newlabel{cref@item:ct:ffeso2}{[enumi][2][](ii)}
\newlabel{cref@item:ct:ipc1}{[enumi][1][](i)}
\newlabel{cref@item:ct:ipc2}{[enumi][2][](ii)}
\newlabel{cref@item:ct:ipc3}{[enumi][3][](iii)}
\newlabel{cref@item:decode-encode-loop-iii}{[enumi][3][](iii)}
\newlabel{cref@item:decode-encode-loop-iv}{[enumi][4][](iv)}
\newlabel{cref@item:ed1}{[enumi][1][](i)}
\newlabel{cref@item:ed2}{[enumi][2][](ii)}
\newlabel{cref@item:ed3}{[enumi][3][](iii)}
\newlabel{cref@item:ed4}{[enumi][4][](iv)}
\newlabel{cref@item:eqvprop2}{[enumi][2][](ii)}
\newlabel{cref@item:eqvprop3}{[enumi][3][](iii)}
\newlabel{cref@item:eqvprop5}{[enumi][5][](v)}
\newlabel{cref@item:fibseq1}{[enumi][1][](i)}
\newlabel{cref@item:fibseq2}{[enumi][2][](ii)}
\newlabel{cref@item:fibseq3}{[enumi][3][](iii)}
\newlabel{cref@item:identity-systems1}{[enumi][1][](i)}
\newlabel{cref@item:identity-systems2}{[enumi][2][](ii)}
\newlabel{cref@item:identity-systems3}{[enumi][3][](iii)}
\newlabel{cref@item:identity-systems4}{[enumi][4][](iv)}
\newlabel{cref@item:mchr1}{[enumi][1][](i)}
\newlabel{cref@item:mchr2}{[enumi][2][](ii)}
\newlabel{cref@item:MLis1}{[enumi][1][](i)}
\newlabel{cref@item:MLis2}{[enumi][2][](ii)}
\newlabel{cref@item:MLis3}{[enumi][3][](iii)}
\newlabel{cref@item:MLis4}{[enumi][4][](iv)}
\newlabel{cref@item:MLis5}{[enumi][5][](v)}
\newlabel{cref@item:modal1}{[enumi][1][](i)}
\newlabel{cref@item:modal2}{[enumi][2][](ii)}
\newlabel{cref@item:modal3}{[enumi][3][](iii)}
\newlabel{cref@item:modal4}{[enumi][4][](iv)}
\newlabel{cref@item:mono1}{[enumi][1][](i)}
\newlabel{cref@item:mono2}{[enumi][3][](iii)}
\newlabel{cref@item:mono3}{[enumi][4][](iv)}
\newlabel{cref@item:mono4}{[enumi][2][](ii)}
\newlabel{cref@item:NO-le-refl}{[enumi][1][](i)}
\newlabel{cref@item:NO-lt-opt}{[enumi][2][](ii)}
\newlabel{cref@item:NO-rec-last}{[enumi][5][](v)}
\newlabel{cref@item:NO-rec-primary}{[enumi][1][](i)}
\newlabel{cref@item:omg1}{[enumi][1][](i)}
\newlabel{cref@item:omg4}{[enumi][4][](iv)}
\newlabel{cref@item:omitcontr1}{[enumi][1][](i)}
\newlabel{cref@item:omitcontr2}{[enumi][2][](ii)}
\newlabel{cref@item:orth-fact-2}{[enumi][2][](ii)}
\newlabel{cref@item:RCltopen1}{[enumi][1][](i)}
\newlabel{cref@item:RCltopen2}{[enumi][2][](ii)}
\newlabel{cref@item:rcrec3}{[enumi][3][](iii)}
\newlabel{cref@item:RC-sim-triangle}{[equation][35][11,3]11.3.35}
\newlabel{cref@item:reg1}{[enumi][1][](i)}
\newlabel{cref@item:reg2}{[enumi][2][](ii)}
\newlabel{cref@item:reg3}{[enumi][3][](iii)}
\newlabel{cref@item:rel1}{[enumi][1][](i)}
\newlabel{cref@item:rel2}{[enumi][2][](ii)}
\newlabel{cref@item:rel3}{[enumi][3][](iii)}
\newlabel{cref@item:sesinj}{[enumi][1][](i)}
\newlabel{cref@item:sesiso}{[enumi][3][](iii)}
\newlabel{cref@item:sessurj}{[enumi][2][](ii)}
\newlabel{cref@item:sigcmp}{[enumi][4][](iv)}
\newlabel{cref@item:sigid}{[enumi][3][](iii)}
\newlabel{cref@item:sim1}{[enumi][1][](i)}
\newlabel{cref@item:sim2}{[enumi][2][](ii)}
\newlabel{cref@item:wh0}{[enumi][1][](i)}
\newlabel{cref@item:whitehead01}{[enumi][1][](i)}
\newlabel{cref@item:whitehead02}{[enumi][2][](ii)}
\newlabel{cref@item:whk}{[enumi][2][](ii)}
\newlabel{cref@item:wop1}{[enumi][1][](i)}
\newlabel{cref@item:wop2}{[enumi][2][](ii)}
\newlabel{cref@lem:ap-functor}{[lem][2][2,2]2.2.2}
\newlabel{cref@lem:autohtpy}{[lem][2][4,1]4.1.2}
\newlabel{cref@lem:BisimEqualsId}{[lem][5][10,5]10.5.5}
\newlabel{cref@lem:coh-equiv}{[lem][2][4,2]4.2.2}
\newlabel{cref@lem:coh-hfib}{[lem][11][4,2]4.2.11}
\newlabel{cref@lem:coh-hprop}{[lem][12][4,2]4.2.12}
\newlabel{cref@lem:concat}{[lem][2][2,1]2.1.2}
\newlabel{cref@lem:connected-map-equiv-truncation}{[lem][14][7,5]7.5.14}
\newlabel{cref@lem:cuts-preserve-admissibility}{[lem][15][11,2]11.2.15}
\newlabel{cref@lem:equiv-iff-hprop}{[lem][3][3,3]3.3.3}
\newlabel{cref@lem:fibration-over-pushout}{[lem][3][8,5]8.5.3}
\newlabel{cref@lem:fullsep}{[lem][10][10,5]10.5.10}
\newlabel{cref@lem:func_retract_to_fiber_retract}{[lem][3][4,7]4.7.3}
\newlabel{cref@lem:hfiber_wrt_pullback}{[lem][8][7,6]7.6.8}
\newlabel{cref@lem:hfib}{[lem][5][4,2]4.2.5}
\newlabel{cref@lem:hlevel-if-inhab-hlevel}{[lem][8][7,2]7.2.8}
\newlabel{cref@lem:homotopy-induction-times-3}{[lem][4][5,5]5.5.4}
\newlabel{cref@lem:homotopy-props}{[lem][2][2,4]2.4.2}
\newlabel{cref@lem:hopf-construction}{[lem][7][8,5]8.5.7}
\newlabel{cref@lem:hspace-S1}{[lem][8][8,5]8.5.8}
\newlabel{cref@lem:htpy-natural}{[lem][3][2,4]2.4.3}
\newlabel{cref@lem:images_are_coequalizers}{[thm][5][10,1]10.1.5}
\newlabel{cref@lem:inv-hprop}{[lem][9][4,2]4.2.9}
\newlabel{cref@lem:mapdep}{[lem][4][2,3]2.3.4}
\newlabel{cref@lem:map}{[lem][1][2,2]2.2.1}
\newlabel{cref@lem:MonicSetPresent}{[lem][6][10,5]10.5.6}
\newlabel{cref@lem:nconnected_postcomp}{[lem][6][7,5]7.5.6}
\newlabel{cref@lem:nconnected_postcomp_variation}{[lem][12][7,5]7.5.12}
\newlabel{cref@lem:nconnected_to_leveln_to_equiv}{[lem][10][7,5]7.5.10}
\newlabel{cref@lem:normal-forms}{[lem][3][2147483647,1,4]A.4.3}
\newlabel{cref@lem:opp}{[lem][1][2,1]2.1.1}
\newlabel{cref@lem:pb_of_coeq_is_coeq}{[lem][6][10,1]10.1.6}
\newlabel{cref@lem:pik-nconnected}{[lem][2][8,3]8.3.2}
\newlabel{cref@lem:qinv-autohtpy}{[lem][1][4,1]4.1.1}
\newlabel{cref@lem:quotient-when-canonical-representatives}{[lem][8][6,10]6.10.8}
\newlabel{cref@lem:s1-decode-encode}{[lem][7][8,1]8.1.7}
\newlabel{cref@lem:s1-encode-decode}{[lem][8][8,1]8.1.8}
\newlabel{cref@lem:sets_exact}{[lem][8][10,1]10.1.8}
\newlabel{cref@lem:susp-loop-adj}{[lem][4][6,5]6.5.4}
\newlabel{cref@lem:transport}{[lem][1][2,3]2.3.1}
\newlabel{cref@lem:transport-s1-code}{[lem][2][8,1]8.1.2}
\newlabel{cref@lem:truncation-le}{[lem][15][7,3]7.3.15}
\newlabel{cref@lem:untruncated-linearity-reals-coincide}{[lem][1][11,4]11.4.1}
\newlabel{cref@mult-from-square}{[equation][45][11,3]11.3.45}
\newlabel{cref@notnotstable-equality-to-set}{[cor][3][7,2]7.2.3}
\newlabel{cref@ordered-field}{[defn][7][11,2]11.2.7}
\newlabel{cref@prop:factor_equiv_fiber}{[lem][5][7,6]7.6.5}
\newlabel{cref@prop:kernels_are_effective}{[thm][9][10,1]10.1.9}
\newlabel{cref@prop:lv_n_deptype_sec_equiv_by_precomp}{[thm][7][7,7]7.7.7}
\newlabel{cref@prop:nat-is-set}{[thm][6][7,2]7.2.6}
\newlabel{cref@prop:nconnected_tested_by_lv_n_dependent types}{[lem][7][7,5]7.5.7}
\newlabel{cref@prop:nconn_fiber_to_total}{[lem][13][7,5]7.5.13}
\newlabel{cref@prop:to_image_is_connected}{[lem][4][7,6]7.6.4}
\newlabel{cref@prop:trunc_of_prop_is_set}{[lem][13][10,1]10.1.13}
\newlabel{cref@RC-archimedean-ordered-field}{[thm][48][11,3]11.3.48}
\newlabel{cref@RC-archimedean}{[thm][41][11,3]11.3.41}
\newlabel{cref@RC-binary-nonexpanding-extension}{[lem][40][11,3]11.3.40}
\newlabel{cref@RC-continuous-eq}{[lem][39][11,3]11.3.39}
\newlabel{cref@RC-extend-Q-Lipschitz}{[lem][15][11,3]11.3.15}
\newlabel{cref@RC-initial-Cauchy-complete}{[thm][50][11,3]11.3.50}
\newlabel{cref@RC-lim-factor}{[lem][11][11,3]11.3.11}
\newlabel{cref@RC-lim-onto}{[lem][10][11,3]11.3.10}
\newlabel{cref@RC-Lipschitz-on-interval}{[ex][8][11]11.8}
\newlabel{cref@RC-sim-eqv-le}{[thm][44][11,3]11.3.44}
\newlabel{cref@RC-sim-rounded}{[equation][21][11,3]11.3.21}
\newlabel{cref@RC-squaring}{[thm][46][11,3]11.3.46}
\newlabel{cref@RD-archimedean-ordered-field}{[thm][8][11,2]11.2.8}
\newlabel{cref@RD-archimedean}{[thm][6][11,2]11.2.6}
\newlabel{cref@RD-cauchy-complete}{[thm][12][11,2]11.2.12}
\newlabel{cref@RD-dedekind-complete}{[cor][16][11,2]11.2.16}
\newlabel{cref@RD-final-field}{[thm][14][11,2]11.2.14}
\newlabel{cref@RD-inverse-apart-0}{[thm][4][11,2]11.2.4}
\newlabel{cref@reals-formal-topology-locally-compact}{[lem][14][11,5]11.5.14}
\newlabel{cref@reflectcommutespushout}{[thm][12][7,4]7.4.12}
\newlabel{cref@rmk:connectedness-indexing}{[rmk][3][7,5]7.5.3}
\newlabel{cref@rmk:defid}{[rmk][1][6,2]6.2.1}
\newlabel{cref@rmk:infty-group}{[rmk][2][6,11]6.11.2}
\newlabel{cref@rmk:introducing-new-concepts}{[rmk][1][1,5]1.5.1}
\newlabel{cref@rmk:naive}{[rmk][3][8,7]8.7.3}
\newlabel{cref@rmk:spokes-no-hub}{[rmk][1][6,7]6.7.1}
\newlabel{cref@rmk:true-neq-false}{[rmk][6][2,12]2.12.6}
\newlabel{cref@rmk:varies-along}{[rmk][4][6,2]6.2.4}
\newlabel{cref@S1-universal-cover}{[defn][1][8,1]8.1.1}
\newlabel{cref@sec:adjunctions}{[section][3][]9.3}
\newlabel{cref@sec:algebr-struct-cauchy}{[subsection][3][]11.3.3}
\newlabel{cref@sec:algebr-struct-dedek}{[subsection][1][]11.2.1}
\newlabel{cref@sec:appetizer-univalence}{[section][2][]5.2}
\newlabel{cref@sec:axiom-choice}{[section][8][]3.8}
\newlabel{cref@sec:axioms}{[section][1][]1.1}
\newlabel{cref@sec:basics-equivalences}{[section][4][]2.4}
\newlabel{cref@sec:basics-sets}{[section][1][]3.1}
\newlabel{cref@sec:better-vankampen}{[subsection][2][]8.7.2}
\newlabel{cref@sec:biinv}{[section][3][]4.3}
\newlabel{cref@sec:bool-nat}{[section][1][]5.1}
\newlabel{cref@sec:cardinals}{[section][2][]10.2}
\newlabel{cref@sec:cats}{[section][1][]9.1}
\newlabel{cref@sec:cauchy-reals-cauchy-complete}{[subsection][4][]11.3.4}
\newlabel{cref@sec:cauchy-reals}{[section][3][]11.3}
\newlabel{cref@sec:cell-complexes}{[section][6][]6.6}
\newlabel{cref@sec:circle}{[section][4][]6.4}
\newlabel{cref@sec:colimits}{[section][8][]6.8}
\newlabel{cref@sec:compactness-interval}{[section][5][]11.5}
\newlabel{cref@sec:comp-cauchy-dedek}{[section][4][]11.4}
\newlabel{cref@sec:computational}{[section][5][]2.5}
\newlabel{cref@sec:compute-cartprod}{[section][6][]2.6}
\newlabel{cref@sec:compute-coprod}{[section][12][]2.12}
\newlabel{cref@sec:compute-nat}{[section][13][]2.13}
\newlabel{cref@sec:compute-paths}{[section][11][]2.11}
\newlabel{cref@sec:compute-pi}{[section][9][]2.9}
\newlabel{cref@sec:compute-sigma}{[section][7][]2.7}
\newlabel{cref@sec:compute-unit}{[section][8][]2.8}
\newlabel{cref@sec:compute-universe}{[section][10][]2.10}
\newlabel{cref@sec:concluding-remarks}{[section][5][]4.5}
\newlabel{cref@sec:connectivity}{[section][5][]7.5}
\newlabel{cref@sec:conn-susp}{[section][2][]8.2}
\newlabel{cref@sec:constr-cauchy-reals}{[subsection][1][]11.3.1}
\newlabel{cref@sec:contractibility}{[section][11][]3.11}
\newlabel{cref@sec:contrf}{[section][4][]4.4}
\newlabel{cref@sec:coproduct-types}{[section][7][]1.7}
\newlabel{cref@sec:cumulative-hierarchy}{[section][5][]10.5}
\newlabel{cref@sec:dagger-categories}{[section][7][]9.7}
\newlabel{cref@sec:dedekind-reals}{[section][2][]11.2}
\newlabel{cref@sec:dependent-paths}{[section][2][]6.2}
\newlabel{cref@sec:disequality}{[subsection][3][]1.12.3}
\newlabel{cref@sec:equality-of-structures}{[section][14][]2.14}
\newlabel{cref@sec:equality}{[section][1][]2.1}
\newlabel{cref@sec:equivalences}{[section][4][]9.4}
\newlabel{cref@sec:equiv-closures}{[section][7][]4.7}
\newlabel{cref@sec:fiberwise-equivalences}{[section][7][]4.7}
\newlabel{cref@sec:fib-over-pushout}{[subsection][1][]8.5.1}
\newlabel{cref@sec:fibrations}{[section][3][]2.3}
\newlabel{cref@sec:field-rati-numb}{[section][1][]11.1}
\newlabel{cref@sec:finite-product-types}{[section][5][]1.5}
\newlabel{cref@sec:flattening}{[section][12][]6.12}
\newlabel{cref@sec:formal-prelim}{[appendix][1][2147483647]A}
\newlabel{cref@sec:free-algebras}{[section][11][]6.11}
\newlabel{cref@sec:freudenthal}{[section][6][]8.6}
\newlabel{cref@sec:function-types}{[section][2][]1.2}
\newlabel{cref@sec:functors}{[section][2][]2.2}
\newlabel{cref@sec:general-encode-decode}{[section][9][]8.9}
\newlabel{cref@sec:generalizations}{[section][7][]5.7}
\newlabel{cref@sec:hae}{[section][2][]4.2}
\newlabel{cref@sec:hedberg}{[section][2][]7.2}
\newlabel{cref@sec:hittruncations}{[section][9][]6.9}
\newlabel{cref@sec:hopf}{[section][5][]8.5}
\newlabel{cref@sec:hott-features}{[section][3][2147483647]A.3}
\newlabel{cref@sec:htpy-inductive}{[section][5][]5.5}
\newlabel{cref@sec:hubs-spokes}{[section][7][]6.7}
\newlabel{cref@sec:identity-systems}{[section][8][]5.8}
\newlabel{cref@sec:identity-types}{[section][12][]1.12}
\newlabel{cref@sec:image-factorization}{[section][6][]7.6}
\newlabel{cref@sec:image}{[subsection][2][]10.1.2}
\newlabel{cref@sec:inductive-types}{[section][9][]1.9}
\newlabel{cref@sec:induct-recurs-cauchy}{[subsection][2][]11.3.2}
\newlabel{cref@sec:initial-alg}{[section][4][]5.4}
\newlabel{cref@sec:interval}{[section][3][]6.3}
\newlabel{cref@sec:intro-hits}{[section][1][]6.1}
\newlabel{cref@sec:intuitionism}{[section][4][]3.4}
\newlabel{cref@sec:long-exact-sequence-homotopy-groups}{[section][4][]8.4}
\newlabel{cref@sec:modalities}{[section][7][]7.7}
\newlabel{cref@sec:mono-surj}{[section][6][]4.6}
\newlabel{cref@sec:more-formal-pi}{[subsection][4][2147483647]A.2.4}
\newlabel{cref@sec:more-formal-sigma}{[subsection][5][2147483647]A.2.5}
\newlabel{cref@sec:moreresults}{[section][10][]8.10}
\newlabel{cref@sec:naive-vankampen}{[subsection][1][]8.7.1}
\newlabel{cref@sec:naturality}{[section][13][]6.13}
\newlabel{cref@sec:n-types}{[section][1][]7.1}
\newlabel{cref@sec:object-classification}{[section][8][]4.8}
\newlabel{cref@sec:ordinals}{[section][3][]10.3}
\newlabel{cref@sec:pat}{[section][11][]1.11}
\newlabel{cref@sec:pattern-matching}{[section][10][]1.10}
\newlabel{cref@sec:pi1s1-classical-proof}{[subsection][2][]8.1.2}
\newlabel{cref@sec:pi1s1-idsys}{[subsection][6][]8.1.6}
\newlabel{cref@sec:pi1s1-initial-thoughts}{[subsection][1][]8.1.1}
\newlabel{cref@sec:pi1-s1-intro}{[section][1][]8.1}
\newlabel{cref@sec:pi1s1-universal-cover}{[subsection][3][]8.1.3}
\newlabel{cref@sec:pik-le-n}{[section][3][]8.3}
\newlabel{cref@sec:pi-types}{[section][4][]1.4}
\newlabel{cref@sec:piw-pretopos}{[section][1][]10.1}
\newlabel{cref@sec:pushouts}{[section][4][]7.4}
\newlabel{cref@sec:quasi-inverses}{[section][1][]4.1}
\newlabel{cref@sec:RD-cauchy-complete}{[subsection][2][]11.2.2}
\newlabel{cref@sec:RD-dedekind-complete}{[subsection][3][]11.2.3}
\newlabel{cref@sec:rezk}{[section][9][]9.9}
\newlabel{cref@sec:set-quotients}{[section][10][]6.10}
\newlabel{cref@sec:sigma-types}{[section][6][]1.6}
\newlabel{cref@sec:sip}{[section][8][]9.8}
\newlabel{cref@sec:strict-categories}{[section][6][]9.6}
\newlabel{cref@sec:strictly-positive}{[section][6][]5.6}
\newlabel{cref@sec:surreals}{[section][6][]11.6}
\newlabel{cref@sec:suspension}{[section][5][]6.5}
\newlabel{cref@sec:syntax-informally}{[section][1][2147483647]A.1}
\newlabel{cref@sec:syntax-more-formally}{[section][2][2147483647]A.2}
\newlabel{cref@sec:transfors}{[section][2][]9.2}
\newlabel{cref@sec:truncations}{[section][3][]7.3}
\newlabel{cref@sec:type-booleans}{[section][8][]1.8}
\newlabel{cref@sec:types-vs-sets}{[section][1][]1.1}
\newlabel{cref@sec:unique-choice}{[section][9][]3.9}
\newlabel{cref@sec:univalence-implies-funext}{[section][9][]4.9}
\newlabel{cref@sec:universal-properties}{[section][15][]2.15}
\newlabel{cref@sec:universes}{[section][3][]1.3}
\newlabel{cref@sec:van-kampen}{[section][7][]8.7}
\newlabel{cref@sec:wellorderings}{[section][4][]10.4}
\newlabel{cref@sec:whitehead}{[section][8][]8.8}
\newlabel{cref@sec:w-types}{[section][3][]5.3}
\newlabel{cref@sec:yoneda}{[section][5][]9.5}
\newlabel{cref@subsec:emacinsets}{[subsection][5][]10.1.5}
\newlabel{cref@subsec:general-remarks}{[cor][7][2147483647,1,4]A.4.7}
\newlabel{cref@subsec:hprops}{[section][3][]3.3}
\newlabel{cref@subsec:limits-sets}{[subsection][1][]10.1.1}
\newlabel{cref@subsec:logic-hprop}{[section][6][]3.6}
\newlabel{cref@subsec:pat?}{[section][2][]3.2}
\newlabel{cref@subsec:pi1s1-encode-decode}{[subsection][4][]8.1.4}
\newlabel{cref@subsec:pi1s1-homotopy-theory}{[subsection][5][]8.1.5}
\newlabel{cref@subsec:piw}{[subsection][4][]10.1.4}
\newlabel{cref@subsec:prop-subsets}{[section][5][]3.5}
\newlabel{cref@subsec:prop-trunc}{[section][7][]3.7}
\newlabel{cref@subsec:quotients}{[subsection][3][]10.1.3}
\newlabel{cref@subsec:when-trunc}{[section][10][]3.10}
\newlabel{cref@tab:homotopy-groups-of-spheres}{[table][1][8]8.1}
\newlabel{cref@tab:pov}{[table][1][0]1}
\newlabel{cref@tab:theorems}{[table][2][8]8.2}
\newlabel{cref@thm:1surj_to_surj_to_pem}{[thm][14][10,1]10.1.14}
\newlabel{cref@thm:ac-epis-split}{[lem][2][3,8]3.8.2}
\newlabel{cref@thm:allbool-trueorfalse}{[thm][1][1,8]1.8.1}
\newlabel{cref@thm:ap2}{[lem][4][6,4]6.4.4}
\newlabel{cref@thm:apd2}{[lem][6][6,4]6.4.6}
\newlabel{cref@thm:apd-const}{[lem][8][2,3]2.3.8}
\newlabel{cref@thm:ap-prod}{[thm][5][2,6]2.6.5}
\newlabel{cref@thm:ap-sigma-rect-path-pair}{[lem][7][6,12]6.12.7}
\newlabel{cref@thm:ap-transport}{[lem][11][2,3]2.3.11}
\newlabel{cref@thm:Cauchy-reals-are-a-set}{[thm][9][11,3]11.3.9}
\newlabel{cref@thm:conemap-funct}{[lem][10][7,4]7.4.10}
\newlabel{cref@thm:connected-pointed}{[lem][11][7,5]7.5.11}
\newlabel{cref@thm:conn-pik}{[cor][8][8,4]8.4.8}
\newlabel{cref@thm:conn-trunc-variable-ind}{[lem][1][8,6]8.6.1}
\newlabel{cref@thm:contr-contr}{[cor][5][3,11]3.11.5}
\newlabel{cref@thm:contr-forall}{[lem][6][3,11]3.11.6}
\newlabel{cref@thm:contr-hae}{[thm][6][4,2]4.2.6}
\newlabel{cref@thm:contr-hprop}{[lem][4][4,4]4.4.4}
\newlabel{cref@thm:contr-paths}{[lem][8][3,11]3.11.8}
\newlabel{cref@thm:contr-unit}{[lem][3][3,11]3.11.3}
\newlabel{cref@thm:conversion-preserves-typing}{[thm][1][2147483647,1,4]A.4.1}
\newlabel{cref@thm:covering-spaces}{[thm][4][8,10]8.10.4}
\newlabel{cref@thm:dpath-arrow}{[lem][6][2,9]2.9.6}
\newlabel{cref@thm:dpath-forall}{[lem][7][2,9]2.9.7}
\newlabel{cref@thm:dpath-path}{[thm][5][2,11]2.11.5}
\newlabel{cref@thm:EckmannHilton}{[thm][6][2,1]2.1.6}
\newlabel{cref@thm:encode-total-equiv}{[cor][13][8,1]8.1.13}
\newlabel{cref@thm:equiv-biinv-isequiv}{[cor][3][4,3]4.3.3}
\newlabel{cref@thm:equiv-compose-equiv}{[lem][8][4,2]4.2.8}
\newlabel{cref@thm:equiv-contr-hae}{[thm][5][4,4]4.4.5}
\newlabel{cref@thm:equiv-eqrel}{[lem][12][2,4]2.4.12}
\newlabel{cref@thm:equiv-induction}{[cor][5][5,8]5.8.5}
\newlabel{cref@thm:equiv-inhabcod}{[cor][6][4,4]4.4.6}
\newlabel{cref@thm:equiv-iso-adj}{[thm][3][4,2]4.2.3}
\newlabel{cref@thm:eta-sigma}{[cor][3][2,7]2.7.3}
\newlabel{cref@thm:ETCS}{[thm][15][10,1]10.1.15}
\newlabel{cref@thm:fiber-of-a-fibration}{[lem][1][4,8]4.8.1}
\newlabel{cref@thm:fiber-of-the-fiber}{[lem][4][8,4]8.4.4}
\newlabel{cref@thm:flattening}{[lem][2][6,12]6.12.2}
\newlabel{cref@thm:flattening-rect}{[lem][4][6,12]6.12.4}
\newlabel{cref@thm:flattening-rectnd-beta-ppt}{[lem][8][6,12]6.12.8}
\newlabel{cref@thm:flattening-rectnd}{[lem][5][6,12]6.12.5}
\newlabel{cref@thm:freegroup-nonset}{[rmk][8][6,11]6.11.8}
\newlabel{cref@thm:free-monoid}{[lem][5][6,11]6.11.5}
\newlabel{cref@thm:freudcode}{[defn][5][8,6]8.6.5}
\newlabel{cref@thm:freudenthal}{[thm][4][8,6]8.6.4}
\newlabel{cref@thm:freudlemma}{[lem][10][8,6]8.6.10}
\newlabel{cref@thm:hae-hprop}{[thm][13][4,2]4.2.13}
\newlabel{cref@thm:hedberg}{[thm][5][7,2]7.2.5}
\newlabel{cref@thm:hlevel-cumulative}{[thm][7][7,1]7.1.7}
\newlabel{cref@thm:hlevel-loops}{[thm][7][7,2]7.2.7}
\newlabel{cref@thm:hleveln-of-hlevelSn}{[thm][11][7,1]7.1.11}
\newlabel{cref@thm:hlevel-prod}{[thm][9][7,1]7.1.9}
\newlabel{cref@thm:h-level-retracts}{[thm][4][7,1]7.1.4}
\newlabel{cref@thm:homotopy-groups}{[eg][4][6,11]6.11.4}
\newlabel{cref@thm:h-set-refrel-in-paths-sets}{[thm][2][7,2]7.2.2}
\newlabel{cref@thm:h-set-uip-K}{[thm][1][7,2]7.2.1}
\newlabel{cref@thm:htpy-induction}{[cor][6][5,8]5.8.6}
\newlabel{cref@thm:identity-systems}{[thm][2][5,8]5.8.2}
\newlabel{cref@thm:inhabprop-eqvunit}{[lem][2][3,3]3.3.2}
\newlabel{cref@thm:injsurj}{[lem][9][10,2]10.2.9}
\newlabel{cref@thm:interval-funext}{[lem][2][6,3]6.3.2}
\newlabel{cref@thm:isaprop-isofhlevel}{[thm][10][7,1]7.1.10}
\newlabel{cref@thm:isntype-mono}{[thm][6][7,1]7.1.6}
\newlabel{cref@thm:isprop-biinv}{[thm][2][4,3]4.3.2}
\newlabel{cref@thm:isprop-forall}{[eg][2][3,6]3.6.2}
\newlabel{cref@thm:isprop-iscontr}{[lem][4][3,11]3.11.4}
\newlabel{cref@thm:isprop-isprop}{[lem][5][3,3]3.3.5}
\newlabel{cref@thm:isprop-isset}{[lem][5][3,3]3.3.5}
\newlabel{cref@thm:isset-forall}{[eg][6][3,1]3.1.6}
\newlabel{cref@thm:isset-is1type}{[lem][8][3,1]3.1.8}
\newlabel{cref@thm:isset-prod}{[eg][5][3,1]3.1.5}
\newlabel{cref@thm:kbar}{[lem][9][8,7]8.7.9}
\newlabel{cref@thm:lequiv-contr-hae}{[thm][3][4,4]4.4.3}
\newlabel{cref@thm:les}{[thm][6][8,4]8.4.6}
\newlabel{cref@thm:loop-nontrivial}{[lem][1][6,4]6.4.1}
\newlabel{cref@thm:looptothe}{[cor][13][6,10]6.10.13}
\newlabel{cref@thm:minusoneconn-surjective}{[lem][2][7,5]7.5.2}
\newlabel{cref@thm:ML-identity-systems}{[thm][4][5,8]5.8.4}
\newlabel{cref@thm:modal-char}{[thm][4][7,7]7.7.4}
\newlabel{cref@thm:modal-mono}{[lem][2][7,6]7.6.2}
\newlabel{cref@thm:mono}{[lem][1][10,1]10.1.1}
\newlabel{cref@thm:mono-surj-equiv}{[thm][3][4,6]4.6.3}
\newlabel{cref@thm:naive-van-kampen}{[thm][4][8,7]8.7.4}
\newlabel{cref@thm:nat-hinitial}{[thm][5][5,4]5.4.5}
\newlabel{cref@thm:nat-set}{[eg][4][3,1]3.1.4}
\newlabel{cref@thm:nat-uniq}{[thm][1][5,1]5.1.1}
\newlabel{cref@thm:nat-wf}{[eg][5][10,3]10.3.5}
\newlabel{cref@thm:nconn-to-ntype-const}{[cor][9][7,5]7.5.9}
\newlabel{cref@thm:nobject-classifier-appetizer}{[thm][3][4,8]4.8.3}
\newlabel{cref@thm:NO-encode-decode}{[thm][16][11,6]11.6.16}
\newlabel{cref@thm:no-higher-ac}{[lem][5][3,8]3.8.5}
\newlabel{cref@thm:NO-refl-opt}{[thm][4][11,6]11.6.4}
\newlabel{cref@thm:NO-set}{[cor][5][11,6]11.6.5}
\newlabel{cref@thm:NO-simplicity}{[thm][2][11,6]11.6.2}
\newlabel{cref@thm:not-dneg}{[thm][2][3,2]3.2.2}
\newlabel{cref@thm:not-lem}{[cor][7][3,2]3.2.7}
\newlabel{cref@thm:NO-unstrict-transitive}{[cor][17][11,6]11.6.17}
\newlabel{cref@thm:ntype-nloop}{[thm][9][7,2]7.2.9}
\newlabel{cref@thm:ntypes-sigma}{[thm][8][7,1]7.1.8}
\newlabel{cref@thm:object-classifier}{[thm][4][4,8]4.8.4}
\newlabel{cref@thm:omg}{[lem][4][2,1]2.1.4}
\newlabel{cref@thm:omit-contr}{[lem][9][3,11]3.11.9}
\newlabel{cref@thm:ordord}{[thm][20][10,3]10.3.20}
\newlabel{cref@thm:ordsucc}{[lem][21][10,3]10.3.21}
\newlabel{cref@thm:ordunion}{[lem][22][10,3]10.3.22}
\newlabel{cref@thm:orth-fact}{[thm][6][7,6]7.6.6}
\newlabel{cref@thm:path-coprod}{[thm][5][2,12]2.12.5}
\newlabel{cref@thm:path-lifting}{[lem][2][2,3]2.3.2}
\newlabel{cref@thm:path-nat}{[thm][1][2,13]2.13.1}
\newlabel{cref@thm:path-prod}{[thm][2][2,6]2.6.2}
\newlabel{cref@thm:path-sigma}{[thm][2][2,7]2.7.2}
\newlabel{cref@thm:paths-respects-equiv}{[thm][1][2,11]2.11.1}
\newlabel{cref@thm:path-subset}{[lem][1][3,5]3.5.1}
\newlabel{cref@thm:path-truncation}{[thm][12][7,3]7.3.12}
\newlabel{cref@thm:path-unit}{[thm][1][2,8]2.8.1}
\newlabel{cref@thm:pi1s1-decode}{[defn][6][8,1]8.1.6}
\newlabel{cref@thm:pik-conn}{[cor][5][8,8]8.8.5}
\newlabel{cref@thm:prod-umpd}{[thm][5][2,15]2.15.5}
\newlabel{cref@thm:prod-ump}{[thm][2][2,15]2.15.2}
\newlabel{cref@thm:prop-minusonetype}{[lem][10][3,11]3.11.10}
\newlabel{cref@thm:prop-set}{[lem][4][3,3]3.3.4}
\newlabel{cref@thm:pushout-ump}{[lem][2][6,8]6.8.2}
\newlabel{cref@thm:quotient-surjective}{[lem][2][6,10]6.10.2}
\newlabel{cref@thm:quotient-ump}{[lem][3][6,10]6.10.3}
\newlabel{cref@thm:RC-le-grow}{[lem][42][11,3]11.3.42}
\newlabel{cref@thm:RC-lt-open}{[lem][43][11,3]11.3.43}
\newlabel{cref@thm:RC-sim-characterization}{[thm][32][11,3]11.3.32}
\newlabel{cref@thm:RC-sim-lim}{[lem][36][11,3]11.3.36}
\newlabel{cref@thm:RC-sim-lim-term}{[lem][37][11,3]11.3.37}
\newlabel{cref@thm:RCsim-symmetric}{[lem][12][11,3]11.3.12}
\newlabel{cref@thm:refl-over-ntype-base}{[cor][10][7,3]7.3.10}
\newlabel{cref@thm:reflsubunv-forall}{[thm][2][7,7]7.7.2}
\newlabel{cref@thm:retract-contr}{[lem][7][3,11]3.11.7}
\newlabel{cref@thm:retract-equiv}{[thm][4][4,7]4.7.4}
\newlabel{cref@thm:retraction-quotient}{[cor][10][6,10]6.10.10}
\newlabel{cref@thm:S1-autohtpy}{[lem][2][6,4]6.4.2}
\newlabel{cref@thm:S1rec}{[lem][5][6,2]6.2.5}
\newlabel{cref@thm:S1ump}{[lem][9][6,2]6.2.9}
\newlabel{cref@thm:ses}{[lem][7][8,4]8.4.7}
\newlabel{cref@thm:set-pushout}{[lem][3][6,9]6.9.3}
\newlabel{cref@thm:set_regular}{[thm][5][10,1]10.1.5}
\newlabel{cref@thm:settopos}{[thm][12][10,1]10.1.12}
\newlabel{cref@thm:sign-induction}{[lem][12][6,10]6.10.12}
\newlabel{cref@thm:sip}{[thm][2][9,8]9.8.2}
\newlabel{cref@thm:stable-images}{[thm][9][7,6]7.6.9}
\newlabel{cref@thm:strong-normalization}{[thm][2][2147483647,1,4]A.4.2}
\newlabel{cref@thm:suspbool}{[lem][1][6,5]6.5.1}
\newlabel{cref@thm:suspension-increases-connectedness}{[thm][1][8,2]8.2.1}
\newlabel{cref@thm:total-fiber-equiv}{[thm][7][4,7]4.7.7}
\newlabel{cref@thm:total-space-of-the-fibers}{[lem][2][4,8]4.8.2}
\newlabel{cref@thm:transport2}{[lem][5][6,4]6.4.5}
\newlabel{cref@thm:transport-compose}{[lem][10][2,3]2.3.10}
\newlabel{cref@thm:transport-concat}{[lem][9][2,3]2.3.9}
\newlabel{cref@thm:transportequiv}{[eg][9][2,4]2.4.9}
\newlabel{cref@thm:transport-is-ap}{[lem][5][2,10]2.10.5}
\newlabel{cref@thm:transport-is-given}{[lem][1][6,12]6.12.1}
\newlabel{cref@thm:transport-path2}{[thm][4][2,11]2.11.4}
\newlabel{cref@thm:transport-path}{[thm][3][2,11]2.11.3}
\newlabel{cref@thm:trans-prod}{[thm][4][2,6]2.6.4}
\newlabel{cref@thm:trans-trivial}{[lem][5][2,3]2.3.5}
\newlabel{cref@thm:trunc0-ind}{[lem][1][6,9]6.9.1}
\newlabel{cref@thm:trunc0-lump}{[lem][2][6,9]6.9.2}
\newlabel{cref@thm:trunc-htpy}{[lem][5][7,3]7.3.5}
\newlabel{cref@thm:trunc-in-truncated-sigma}{[thm][9][7,3]7.3.9}
\newlabel{cref@thm:truncn-ind}{[thm][2][7,3]7.3.2}
\newlabel{cref@thm:trunc-reflective}{[lem][3][7,3]7.3.3}
\newlabel{cref@thm:ttac}{[thm][7][2,15]2.15.7}
\newlabel{cref@thm:two-out-of-three}{[thm][1][4,7]4.7.1}
\newlabel{cref@thm:type-is-not-a-set}{[eg][9][3,1]3.1.9}
\newlabel{cref@thm:van-Kampen}{[thm][12][8,7]8.7.12}
\newlabel{cref@thm:VisCST}{[thm][8][10,5]10.5.8}
\newlabel{cref@thm:wedge-connectivity}{[lem][2][8,6]8.6.2}
\newlabel{cref@thm:wellorder}{[thm][3][10,4]10.4.3}
\newlabel{cref@thm:wfcat}{[cor][15][10,3]10.3.15}
\newlabel{cref@thm:wfmin}{[lem][8][10,3]10.3.8}
\newlabel{cref@thm:wfrec}{[lem][7][10,3]10.3.7}
\newlabel{cref@thm:w-hinit}{[thm][7][5,4]5.4.7}
\newlabel{cref@thm:whitehead0}{[thm][1][8,8]8.8.1}
\newlabel{cref@thm:whitehead1}{[cor][2][8,8]8.8.2}
\newlabel{cref@thm:whitehead-contr}{[cor][4][8,8]8.8.4}
\newlabel{cref@thm:whiteheadn}{[thm][3][8,8]8.8.3}
\newlabel{cref@thm:wop}{[thm][4][10,4]10.4.4}
\newlabel{cref@thm:wtype-wf}{[eg][6][10,3]10.3.6}
\newlabel{cref@thm:w-uniq}{[thm][1][5,3]5.3.1}
\newlabel{cref@thm:zfc}{[thm][11][10,5]10.5.11}
\newlabel{cref@transport-Sigma}{[thm][4][2,7]2.7.4}
\newlabel{cref@UA-eqv-hom-eqv}{[lem][2][4,9]4.9.2}
\newlabel{cref@uatowfe}{[thm][4][4,9]4.9.4}
\newlabel{cref@weakfunext}{[defn][1][4,9]4.9.1}
\newlabel{cref@wfetofe}{[thm][5][4,9]4.9.5}
\newlabel{cref@when-reals-coincide}{[cor][3][11,4]11.4.3}
\newlabel{cref@Z-quotient-by-canonical-representatives}{[rmk][11][6,10]6.10.11}
\newlabel{ct:2cat}{9.5}
\newlabel{ct:adjointification}{9.4.2}
\newlabel{ct:adjprop2}{9.5.11}
\newlabel{ct:adjprop}{9.3.2}
\newlabel{ct:adj-repr}{9.5.10}
\newlabel{ctb-uniformly-continuous-sup}{11.5.7}
\newlabel{ct:cat-2cat}{9.4.16}
\newlabel{ct:category}{9.1.6}
\newlabel{ct:cat-eq-iso}{9.4.15}
\newlabel{ct:catweq}{9.4.7}
\newlabel{ct:cat-weq-eq}{9.9.4}
\newlabel{ct:chaotic}{9.4.13}
\newlabel{ct:discrete}{9.1.16}
\newlabel{ct:eg:set}{9.1.7}
\newlabel{ct:equiv}{9.4.1}
\newlabel{ct:eqv-levelwise}{9.4.14}
\newlabel{ct:esofull-precomp-ff}{9.9.2}
\newlabel{ct:ex:hocat}{9.9}
\newlabel{ct:ffeso}{9.4.5}
\newlabel{ct:functor}{9.2.1}
\newlabel{ct:functor-assoc}{9.2.9}
\newlabel{ct:functor-cat}{9.2.5}
\newlabel{ct:functorexpadj}{9.5.3}
\newlabel{ct:functor-precat}{9.2.3}
\newlabel{ct:fundgpd}{9.1.17}
\newlabel{ct:galois}{9.6.3}
\newlabel{ct:gaunt}{9.1.15}
\newlabel{ct:groupoids}{9.6}
\newlabel{ct:hilb}{9.7.7}
\newlabel{ct:hocat}{9.9.7}
\newlabel{ct:hoprecat}{9.1.18}
\newlabel{ct:idtoiso}{9.1.4}
\newlabel{ct:idtoisocompute}{9.1.10}
\newlabel{ct:idtoiso-trans}{9.1.9}
\newlabel{ct:idtounitary}{9.7.3}
\newlabel{ct:interchange}{9.2.8}
\newlabel{ct:isocat}{9.4.8}
\newlabel{ct:isomorphism}{9.1.2}
\newlabel{ct:isoprecat}{9.4.9}
\newlabel{ct:isoprop}{9.1.3}
\newlabel{ct:natiso}{9.2.4}
\newlabel{ct:nattrans}{9.2.2}
\newlabel{ct:obj-1type}{9.1.8}
\newlabel{ct:opposite-category}{9.5.1}
\newlabel{ct:orders}{9.1.14}
\newlabel{ct:pentagon}{9.2.10}
\newlabel{ct:pre2cat}{9.4}
\newlabel{ct:precategory}{9.1.1}
\newlabel{ct:precatset}{9.1.5}
\newlabel{ct:rel}{9.1.19}
\newlabel{ct:representable}{9.5.8}
\newlabel{ct:representable-prop}{9.5.9}
\newlabel{ct:rezk-fundgpd-trunc1}{9.9.6}
\newlabel{ct:sig}{9.8.1}
\newlabel{ct:sip-functor-cat}{9.8.3}
\newlabel{ct:unitary}{9.7.2}
\newlabel{ct:units}{9.2.11}
\newlabel{ct:yoneda}{9.5.4}
\newlabel{ct:yoneda-embedding}{9.5.6}
\newlabel{ct:yoneda-mono}{9.5.7}
\newlabel{dedekind-in-cut-as-le}{11.2.2}
\newlabel{def:bisimulation}{10.5.4}
\newlabel{def:hlevel}{7.1.1}
\newlabel{def:loopspace}{2.1.8}
\newlabel{defn:1type}{3.1.7}
\newlabel{defn:accessibility}{10.3.1}
\newlabel{defn:biinv}{4.3.1}
\newlabel{defn:card}{10.2.1}
\newlabel{defn:cauchy-approximation}{11.2.10}
\newlabel{defn:cauchy-reals}{11.3.2}
\newlabel{defn:cocone}{6.8.1}
\newlabel{defn:complete-metric-space}{11.5.2}
\newlabel{defn:contractible}{3.11.1}
\newlabel{defn:decidable-equality}{3.4.3}
\newlabel{defn:dedekind-reals}{11.2.1}
\newlabel{defn:equivalence}{4.4.1}
\newlabel{defn:fo-notion-of-structure}{9.8.4}
\newlabel{defn:homotopy}{2.4.1}
\newlabel{defn:homotopy-fiber}{4.2.4}
\newlabel{defn:identity-systems}{5.8.1}
\newlabel{defn:inductive-cover}{11.5.13}
\newlabel{defn:inductive-cover-interval-1}{(v)}
\newlabel{defn:inductive-cover-interval-2}{(vi)}
\newlabel{defn:ishae}{4.2.1}
\newlabel{defn:isprop}{3.3.1}
\newlabel{defn:lcoh-rcoh}{4.2.10}
\newlabel{defn:linv-rinv}{4.2.7}
\newlabel{defn:lipschitz}{11.3.14}
\newlabel{defn:logical-notation}{3.7.1}
\newlabel{defn:metric-space}{11.5.1}
\newlabel{defn:modal-image}{7.6.3}
\newlabel{defn:modality}{7.7.5}
\newlabel{defn:nalg}{5.4.1}
\newlabel{defn:nhom}{5.4.2}
\newlabel{defn:No-codes}{11.6.7}
\newlabel{defn:RC-approx}{11.3.16}
\newlabel{defn:reflective-subuniverse}{7.7.1}
\newlabel{defn:retract}{4.7.2}
\newlabel{defn:set}{3.1.1}
\newlabel{defn:setof}{3.5}
\newlabel{defn:surreals}{11.6.1}
\newlabel{defn:total-bounded-metric-space}{11.5.3}
\newlabel{defn:total-map}{4.7.5}
\newlabel{defn:uniformly-continuous}{11.5.5}
\newlabel{defn:V}{10.5.1}
\newlabel{defn-Z}{6.10.7}
\newlabel{def-of-homotopy-groups}{8.0.1}
\newlabel{def:pointedmap}{8.4.1}
\newlabel{def:pointedtype}{2.1.7}
\newlabel{def:simulation}{10.3.11}
\newlabel{def:TypeOfElements}{10.5.7}
\newlabel{def:VVquotient}{6.10.5}
\newlabel{eg:circle}{8.7.6}
\newlabel{eg:clvk}{8.7.13}
\newlabel{eg:cofiber}{8.7.14}
\newlabel{eg:concatequiv}{2.4.8}
\newlabel{eg:idequiv}{2.4.7}
\newlabel{eg:kg1}{8.7.17}
\newlabel{eg:suspension}{8.7.7}
\newlabel{eg:torus}{8.7.15}
\newlabel{eg:unnatural-hit}{6.13.1}
\newlabel{eg:wedge}{8.7.8}
\newlabel{Eilenberg-Mac-Lane-Spaces}{8.10.3}
\newlabel{epis-surj}{10.1.4}
\newlabel{eq:ac}{3.8.1}
\newlabel{eq:apd-to-ap}{2.3.7}
\newlabel{eq:appxrec2}{11.3.24}
\newlabel{eq:ap-to-apd}{2.3.6}
\newlabel{eq:bfa-bga2}{8.7.11}
\newlabel{eq:bfa-bga}{8.7.1}
\newlabel{eq:bfa-bga-comm}{8.7.2}
\newlabel{eq:cauchy-approx}{11.2.11}
\newlabel{eq:cauchy-sequence}{11.2.9}
\newlabel{eq:class-notation}{10.5.3}
\newlabel{eq:composeconefunc}{7.4.4}
\newlabel{eq:composeconeid}{7.4.3}
\newlabel{eq:concatD}{2.1.3}
\newlabel{eq:conetrunc}{7.4.11}
\newlabel{eq:cover-pointwise}{11.5.12}
\newlabel{eq:cover-pointwise-truncated}{11.5.10}
\newlabel{eq:ct:gbar}{9.4.12}
\newlabel{eq:ct:ipctri}{9.4.11}
\newlabel{eq:ct:isoprecattri}{9.4.10}
\newlabel{eq:dbl0}{1.10.1}
\newlabel{eq:dbl-as-rec}{1.9.1}
\newlabel{eq:dblsuc}{1.10.2}
\newlabel{eq:decode}{8.7.5}
\newlabel{eq:defn-pullback}{2.15.11}
\newlabel{eq:depCauchyappx}{11.3.5}
\newlabel{eq:dnshift}{3.11.11}
\newlabel{eq:dpath}{6.2.2}
\newlabel{eq:english-ac}{3.2.1}
\newlabel{eq:epis-split}{3.8.3}
\newlabel{eq:equality-semigroup-mult}{2.14.2}
\newlabel{eq:eqv}{2.4.11}
\newlabel{eq:example-comp}{5.6.6}
\newlabel{eq:example-constructor}{5.6.4}
\newlabel{eq:example-indhyp}{5.6.7}
\newlabel{eq:example-rechyp}{5.6.5}
\newlabel{eq:expldef}{1.2.1}
\newlabel{eq:fake-recursor}{5.6.1}
\newlabel{eq:ffprime-north}{6.5.5}
\newlabel{eq:flattening-rectnd}{6.12.6}
\newlabel{eq:fpaut}{3.2.3}
\newlabel{eq:fpfaut}{3.2.4}
\newlabel{eq:freudcode}{8.6.6}
\newlabel{eq:freudcodeN}{8.6.7}
\newlabel{eq:freudcodeS}{8.6.8}
\newlabel{eq:freudcompute1}{8.6.11}
\newlabel{eq:freudcompute2}{8.6.12}
\newlabel{eq:freudenthal-for-spheres}{8.6.16}
\newlabel{eq:freudgoal}{8.6.13}
\newlabel{eq:freudmap}{8.6.9}
\newlabel{eq:fullprop}{9.9.3}
\newlabel{eq:happly}{2.9.2}
\newlabel{eq:injective}{4.6.2}
\newlabel{eq:inlinj}{2.12.1}
\newlabel{eq:inlrdj}{2.12.3}
\newlabel{eq:iscontrf}{4.4.2}
\newlabel{eq:isequiv-invertible}{2.4.10}
\newlabel{eq:Jconv}{2.0.1}
\newlabel{eq:lambda-abstraction}{1.4.1}
\newlabel{eq:ldn}{3.4.2}
\newlabel{eq:lem}{3.4.1}
\newlabel{eq:lpo}{11.5.8}
\newlabel{eq:mapofspans-htpy}{7.4.9}
\newlabel{eq:modaltype}{7.7.6}
\newlabel{eq:NO-codes-transitivity}{11.6.9}
\newlabel{eq:NO-codes-unstrict}{11.6.8}
\newlabel{eq:noind1}{11.6.3}
\newlabel{eq:NO-prec-def}{11.6.15}
\newlabel{eq:NO-preceq-def}{11.6.14}
\newlabel{eq:NO-prec-IHL}{11.6.12}
\newlabel{eq:NO-prec-IHR}{11.6.13}
\newlabel{eq:NO-prec-outer-IH}{11.6.10}
\newlabel{eq:path-forall}{2.9.1}
\newlabel{eq:path-lump}{2.15.10}
\newlabel{eq:path-prod}{2.6.1}
\newlabel{eq:path-prod-inverse}{2.6.3}
\newlabel{eq:path-trunc-map}{7.3.11}
\newlabel{eq:pi1s1-decode}{8.1.4}
\newlabel{eq:pi1s1-encode}{8.1.3}
\newlabel{eq:Pinj}{5.6.2}
\newlabel{eq:polyfunc}{5.4.6}
\newlabel{eq:prodeqv}{2.5.1}
\newlabel{eq:prod-umpd-map}{2.15.4}
\newlabel{eq:prod-ump-map}{2.15.1}
\newlabel{eq:prod-ump-rt1}{2.15.3}
\newlabel{eq:prod-ump-rt2}{2.15.8}
\newlabel{eq:prop-up}{3.5.4}
\newlabel{eq:qinvtype}{2.4.5}
\newlabel{eq:quotient-when-canonical}{6.10.9}
\newlabel{eq:RCappx1}{11.3.17}
\newlabel{eq:RCappx2}{11.3.18}
\newlabel{eq:RCappx3}{11.3.19}
\newlabel{eq:RCappx4}{11.3.20}
\newlabel{eq:RCappx-rtri-rll1}{11.3.29}
\newlabel{eq:RCappx-rtri-rll2}{11.3.30}
\newlabel{eq:RCappx-rtri-rll3}{11.3.31}
\newlabel{eq:RCappx-rtri-rlr1}{11.3.27}
\newlabel{eq:RCappx-rtri-rlr2}{11.3.28}
\newlabel{eq:RCappx-rtri-rrl1}{11.3.25}
\newlabel{eq:RCappx-rtri-rrl2}{11.3.26}
\newlabel{eq:RC-cauchy}{11.3.3}
\newlabel{eq:RC-path}{11.3.4}
\newlabel{eq:rcsimind1}{11.3.6}
\newlabel{eq:rcsimind2}{11.3.7}
\newlabel{eq:RC-sim-ltri}{11.3.23}
\newlabel{eq:RC-sim-recursion-extra}{11.3.13}
\newlabel{eq:RC-sim-rtri}{11.3.22}
\newlabel{eq:RD-linear-order}{11.2.3}
\newlabel{eq:S1recindbase}{6.2.6}
\newlabel{eq:S1recindloop}{6.2.7}
\newlabel{eq:set-up}{3.5.3}
\newlabel{eq:sigma-lump}{2.15.9}
\newlabel{eq:sigma-ump-map}{2.15.6}
\newlabel{eq:Snsusp}{6.5.2}
\newlabel{eq:subset}{3.5.2}
\newlabel{eq:suc-injective}{2.13.3}
\newlabel{eq:sumcodefam}{2.12.4}
\newlabel{eq:tautology1}{1.11.1}
\newlabel{eq:tautology2}{1.11.2}
\newlabel{eq:transport-arrow}{2.9.4}
\newlabel{eq:transport-arrow-families}{2.9.5}
\newlabel{eq:transport-semigroup-assoc}{2.14.3}
\newlabel{eq:transport-semigroup-step1}{2.14.2}
\newlabel{eq:trunc-htpy}{7.3.6}
\newlabel{eq:trunc-nat}{7.3.4}
\newlabel{eq:uatofeps}{4.9.7}
\newlabel{eq:uatofesp}{4.9.6}
\newlabel{eq:uidtoeqv}{2.10.2}
\newlabel{eq:untruncated-linearity}{11.4.2}
\newlabel{equ:prequired}{5.4.8}
\newlabel{eq:V-path}{10.5.2}
\newlabel{eq:yoneda}{9.5.5}
\newlabel{eq:zero-not-succ}{2.13.2}
\newlabel{ex:acconn}{7.10}
\newlabel{ex:ackermann}{1.10}
\newlabel{ex:acnm}{7.8}
\newlabel{ex:acnm-surjset}{7.9}
\newlabel{ex:ap-path-inversion}{8.6}
\newlabel{ex:ap-sigma}{2.7}
\newlabel{ex:basics:concat}{2.1}
\newlabel{ex:bool}{5.4}
\newlabel{ex:brck-qinv}{3.8}
\newlabel{ex:choice-function}{10.10}
\newlabel{ex:composition}{1.1}
\newlabel{ex:connectivity-inductively}{7.6}
\newlabel{ex:coprod-ump}{2.9}
\newlabel{ex:cumhierhit}{10.11}
\newlabel{ex:decidable-choice}{3.19}
\newlabel{ex:disjoint-or}{3.7}
\newlabel{ex:equality-reflection}{2.14}
\newlabel{ex:equiv-concat}{2.6}
\newlabel{ex:eqvboolbool}{2.13}
\newlabel{ex:fin}{1.9}
\newlabel{ex:finite-cover-lebesgue-number}{11.12}
\newlabel{ex:free-monoid}{6.8}
\newlabel{ex:HopfJr}{8.8}
\newlabel{ex:impred-brck}{3.15}
\newlabel{ex:isset-coprod}{3.2}
\newlabel{ex:isset-sigma}{3.3}
\newlabel{ex:lem-brck}{3.14}
\newlabel{ex:lem-impred}{3.10}
\newlabel{ex:lem-ldn}{3.18}
\newlabel{ex:lem-mereprop}{3.6}
\newlabel{ex:lemnm}{7.7}
\newlabel{ex:loop2}{5.8}
\newlabel{ex:loop}{5.7}
\newlabel{ex:mean-value-theorem}{11.13}
\newlabel{ex:metric-completion}{11.9}
\newlabel{ex:neg-ldn}{1.11}
\newlabel{ex:ninf-ord}{10.8}
\newlabel{ex:not-not-lem}{1.13}
\newlabel{ex:npaths}{2.4}
\newlabel{ex:nspheres}{6.4}
\newlabel{ex:ntype-from-nconn-const}{7.5}
\newlabel{ex:ntypes-closed-under-wtypes}{7.3}
\newlabel{ex:omit-contr2}{3.20}
\newlabel{ex:one-function-two-recurrences}{5.3}
\newlabel{ex:pm-to-ml}{1.7}
\newlabel{ex:pointed-equivalences}{8.7}
\newlabel{ex:prod-via-bool}{1.6}
\newlabel{ex:prop-endocontr}{3.4}
\newlabel{ex:prop-inhabcontr}{3.5}
\newlabel{ex:prop-ord}{10.7}
\newlabel{ex:prop-trunc-ind}{3.17}
\newlabel{ex:pullback}{2.11}
\newlabel{ex:pullback-pasting}{2.12}
\newlabel{ex:qinv-autohtpy-no-univalence}{4.3}
\newlabel{ex:RD-extended-reals}{11.2}
\newlabel{ex:RD-interval-arithmetic}{11.4}
\newlabel{ex:RD-lower-cuts}{11.3}
\newlabel{ex:RD-lt-vs-le}{11.5}
\newlabel{ex:reals-apart-neq-MP}{11.10}
\newlabel{ex:reals-apart-zero-divisors}{11.11}
\newlabel{ex:reals-non-constant-into-Z}{11.6}
\newlabel{ex:rezk-vankampen}{9.11}
\newlabel{ex:s2-colim-unit}{7.2}
\newlabel{ex:same-recurrence-not-defeq}{5.2}
\newlabel{ex:sigma-assoc}{2.10}
\newlabel{ex:stack}{9.12}
\newlabel{ex:subtFromPathInd}{1.15}
\newlabel{ex:sum-via-bool}{1.5}
\newlabel{ex:SuperHopf}{8.9}
\newlabel{ex:suspS1}{6.2}
\newlabel{ex:tautologies}{1.12}
\newlabel{ex:torus}{6.1}
\newlabel{ex:torus-s1-times-s1}{6.3}
\newlabel{ex:traditional-archimedean}{11.7}
\newlabel{ex:unique-fiber}{8.5}
\newlabel{ex:unnatural-endomorphisms}{6.9}
\newlabel{ex:unstable-octahedron}{4.4}
\newlabel{ex:vksuspnopt}{8.11}
\newlabel{ex:vksusppt}{8.10}
\newlabel{ex:well-pointed}{10.3}
\newlabel{ex:without-K}{1.14}
\newlabel{fibwise-fiber-total-fiber-equiv}{4.7.6}
\newlabel{fig:hub-and-spokes}{6.3}
\newlabel{fig:spokes-no-hub}{6.4}
\newlabel{fig:spokes-no-hub-ii}{6.5}
\newlabel{fig:topS1ind}{6.1}
\newlabel{fig:ttS1ind}{6.2}
\newlabel{fig:winding}{8.1}
\newlabel{inductive-cover-classical}{11.5.16}
\newlabel{interval-Heine-Borel}{11.5.15}
\newlabel{item:apfunctor-compose}{(iii)}
\newlabel{item:apfunctor-ct}{(i)}
\newlabel{item:apfunctor-opp}{(ii)}
\newlabel{item:autohtpy1}{(i)}
\newlabel{item:autohtpy2}{(ii)}
\newlabel{item:autohtpy3}{(iii)}
\newlabel{item:be1}{(i)}
\newlabel{item:be2}{(ii)}
\newlabel{item:be3}{(iii)}
\newlabel{item:beb1}{(i)}
\newlabel{item:beb2}{(ii)}
\newlabel{item:beb3}{(iii)}
\newlabel{item:cle-inj}{(i)}
\newlabel{item:cle-surj}{(ii)}
\newlabel{item:conntest1}{(i)}
\newlabel{item:conntest2}{(ii)}
\newlabel{item:conntest3}{(iii)}
\newlabel{item:contr-eqv-unit}{(iii)}
\newlabel{item:contr}{(i)}
\newlabel{item:contr-inhabited-prop}{(ii)}
\newlabel{item:conway1}{(i)}
\newlabel{item:conway2}{(ii)}
\newlabel{item:ct:ar1}{(i)}
\newlabel{item:ct:ar2}{(ii)}
\newlabel{item:ct:ffeso1}{(i)}
\newlabel{item:ct:ffeso2}{(ii)}
\newlabel{item:ct:ipc1}{(i)}
\newlabel{item:ct:ipc2}{(ii)}
\newlabel{item:ct:ipc3}{(iii)}
\newlabel{item:decode-encode-loop-iii}{(iii)}
\newlabel{item:decode-encode-loop-iv}{(iv)}
\newlabel{item:ed1}{(i)}
\newlabel{item:ed2}{(ii)}
\newlabel{item:ed3}{(iii)}
\newlabel{item:ed4}{(iv)}
\newlabel{item:eqvprop2}{(ii)}
\newlabel{item:eqvprop3}{(iii)}
\newlabel{item:eqvprop5}{(v)}
\newlabel{item:fibseq1}{(i)}
\newlabel{item:fibseq2}{(ii)}
\newlabel{item:fibseq3}{(iii)}
\newlabel{item:identity-systems1}{(i)}
\newlabel{item:identity-systems2}{(ii)}
\newlabel{item:identity-systems3}{(iii)}
\newlabel{item:identity-systems4}{(iv)}
\newlabel{item:mchr1}{(i)}
\newlabel{item:mchr2}{(ii)}
\newlabel{item:MLis1}{(i)}
\newlabel{item:MLis2}{(ii)}
\newlabel{item:MLis3}{(iii)}
\newlabel{item:MLis4}{(iv)}
\newlabel{item:MLis5}{(v)}
\newlabel{item:modal1}{(i)}
\newlabel{item:modal2}{(ii)}
\newlabel{item:modal3}{(iii)}
\newlabel{item:modal4}{(iv)}
\newlabel{item:mono1}{(i)}
\newlabel{item:mono2}{(iii)}
\newlabel{item:mono3}{(iv)}
\newlabel{item:mono4}{(ii)}
\newlabel{item:NO-le-refl}{(i)}
\newlabel{item:NO-lt-opt}{(ii)}
\newlabel{item:NO-rec-last}{(v)}
\newlabel{item:NO-rec-primary}{(i)}
\newlabel{item:omg1}{(i)}
\newlabel{item:omg4}{(iv)}
\newlabel{item:omitcontr1}{(i)}
\newlabel{item:omitcontr2}{(ii)}
\newlabel{item:orth-fact-2}{(ii)}
\newlabel{item:RCltopen1}{(i)}
\newlabel{item:RCltopen2}{(ii)}
\newlabel{item:rcrec3}{(iii)}
\newlabel{item:RC-sim-triangle}{11.3.35}
\newlabel{item:reg1}{(i)}
\newlabel{item:reg2}{(ii)}
\newlabel{item:reg3}{(iii)}
\newlabel{item:rel1}{(i)}
\newlabel{item:rel2}{(ii)}
\newlabel{item:rel3}{(iii)}
\newlabel{item:sesinj}{(i)}
\newlabel{item:sesiso}{(iii)}
\newlabel{item:sessurj}{(ii)}
\newlabel{item:sigcmp}{(iv)}
\newlabel{item:sigid}{(iii)}
\newlabel{item:sim1}{(i)}
\newlabel{item:sim2}{(ii)}
\newlabel{item:wh0}{(i)}
\newlabel{item:whitehead01}{(i)}
\newlabel{item:whitehead02}{(ii)}
\newlabel{item:whk}{(ii)}
\newlabel{item:wop1}{(i)}
\newlabel{item:wop2}{(ii)}
\newlabel{lem:ap-functor}{2.2.2}
\newlabel{lem:autohtpy}{4.1.2}
\newlabel{lem:BisimEqualsId}{10.5.5}
\newlabel{lem:coh-equiv}{4.2.2}
\newlabel{lem:coh-hfib}{4.2.11}
\newlabel{lem:coh-hprop}{4.2.12}
\newlabel{lem:concat}{2.1.2}
\newlabel{lem:connected-map-equiv-truncation}{7.5.14}
\newlabel{lem:cuts-preserve-admissibility}{11.2.15}
\newlabel{lem:equiv-iff-hprop}{3.3.3}
\newlabel{lem:fibration-over-pushout}{8.5.3}
\newlabel{lem:fullsep}{10.5.10}
\newlabel{lem:func_retract_to_fiber_retract}{4.7.3}
\newlabel{lem:hfib}{4.2.5}
\newlabel{lem:hfiber_wrt_pullback}{7.6.8}
\newlabel{lem:hlevel-if-inhab-hlevel}{7.2.8}
\newlabel{lem:homotopy-induction-times-3}{5.5.4}
\newlabel{lem:homotopy-props}{2.4.2}
\newlabel{lem:hopf-construction}{8.5.7}
\newlabel{lem:hspace-S1}{8.5.8}
\newlabel{lem:htpy-natural}{2.4.3}
\newlabel{lem:images_are_coequalizers}{10.1.5}
\newlabel{lem:inv-hprop}{4.2.9}
\newlabel{lem:map}{2.2.1}
\newlabel{lem:mapdep}{2.3.4}
\newlabel{lem:MonicSetPresent}{10.5.6}
\newlabel{lem:nconnected_postcomp}{7.5.6}
\newlabel{lem:nconnected_postcomp_variation}{7.5.12}
\newlabel{lem:nconnected_to_leveln_to_equiv}{7.5.10}
\newlabel{lem:normal-forms}{A.4.3}
\newlabel{lem:opp}{2.1.1}
\newlabel{lem:pb_of_coeq_is_coeq}{10.1.6}
\newlabel{lem:pik-nconnected}{8.3.2}
\newlabel{lem:qinv-autohtpy}{4.1.1}
\newlabel{lem:quotient-when-canonical-representatives}{6.10.8}
\newlabel{lem:s1-decode-encode}{8.1.7}
\newlabel{lem:s1-encode-decode}{8.1.8}
\newlabel{lem:sets_exact}{10.1.8}
\newlabel{lem:susp-loop-adj}{6.5.4}
\newlabel{lem:transport}{2.3.1}
\newlabel{lem:transport-s1-code}{8.1.2}
\newlabel{lem:truncation-le}{7.3.15}
\newlabel{lem:untruncated-linearity-reals-coincide}{11.4.1}
\newlabel{mult-from-square}{11.3.45}
\newlabel{notnotstable-equality-to-set}{7.2.3}
\newlabel{ordered-field}{11.2.7}
\newlabel{prop:factor_equiv_fiber}{7.6.5}
\newlabel{prop:kernels_are_effective}{10.1.9}
\newlabel{prop:lv_n_deptype_sec_equiv_by_precomp}{7.7.7}
\newlabel{prop:nat-is-set}{7.2.6}
\newlabel{prop:nconnected_tested_by_lv_n_dependent types}{7.5.7}
\newlabel{prop:nconn_fiber_to_total}{7.5.13}
\newlabel{prop:to_image_is_connected}{7.6.4}
\newlabel{prop:trunc_of_prop_is_set}{10.1.13}
\newlabel{RC-archimedean}{11.3.41}
\newlabel{RC-archimedean-ordered-field}{11.3.48}
\newlabel{RC-binary-nonexpanding-extension}{11.3.40}
\newlabel{RC-continuous-eq}{11.3.39}
\newlabel{RC-extend-Q-Lipschitz}{11.3.15}
\newlabel{RC-initial-Cauchy-complete}{11.3.50}
\newlabel{RC-lim-factor}{11.3.11}
\newlabel{RC-lim-onto}{11.3.10}
\newlabel{RC-Lipschitz-on-interval}{11.8}
\newlabel{RC-sim-eqv-le}{11.3.44}
\newlabel{RC-sim-rounded}{11.3.21}
\newlabel{RC-squaring}{11.3.46}
\newlabel{RD-archimedean}{11.2.6}
\newlabel{RD-archimedean-ordered-field}{11.2.8}
\newlabel{RD-cauchy-complete}{11.2.12}
\newlabel{RD-dedekind-complete}{11.2.16}
\newlabel{RD-final-field}{11.2.14}
\newlabel{RD-inverse-apart-0}{11.2.4}
\newlabel{reals-formal-topology-locally-compact}{11.5.14}
\newlabel{reflectcommutespushout}{7.4.12}
\newlabel{rmk:connectedness-indexing}{7.5.3}
\newlabel{rmk:defid}{6.2.1}
\newlabel{rmk:infty-group}{6.11.2}
\newlabel{rmk:introducing-new-concepts}{1.5.1}
\newlabel{rmk:naive}{8.7.3}
\newlabel{rmk:spokes-no-hub}{6.7.1}
\newlabel{rmk:true-neq-false}{2.12.6}
\newlabel{rmk:varies-along}{6.2.4}
\newlabel{S1-universal-cover}{8.1.1}
\newlabel{sec:adjunctions}{9.3}
\newlabel{sec:algebr-struct-cauchy}{11.3.3}
\newlabel{sec:algebr-struct-dedek}{11.2.1}
\newlabel{sec:appetizer-univalence}{5.2}
\newlabel{sec:axiom-choice}{3.8}
\newlabel{sec:axioms}{1.1}
\newlabel{sec:basics-equivalences}{2.4}
\newlabel{sec:basics-sets}{3.1}
\newlabel{sec:better-vankampen}{8.7.2}
\newlabel{sec:biinv}{4.3}
\newlabel{sec:bool-nat}{5.1}
\newlabel{sec:cardinals}{10.2}
\newlabel{sec:cats}{9.1}
\newlabel{sec:cauchy-reals}{11.3}
\newlabel{sec:cauchy-reals-cauchy-complete}{11.3.4}
\newlabel{sec:cell-complexes}{6.6}
\newlabel{sec:circle}{6.4}
\newlabel{sec:colimits}{6.8}
\newlabel{sec:compactness-interval}{11.5}
\newlabel{sec:comp-cauchy-dedek}{11.4}
\newlabel{sec:computational}{2.5}
\newlabel{sec:compute-cartprod}{2.6}
\newlabel{sec:compute-coprod}{2.12}
\newlabel{sec:compute-nat}{2.13}
\newlabel{sec:compute-paths}{2.11}
\newlabel{sec:compute-pi}{2.9}
\newlabel{sec:compute-sigma}{2.7}
\newlabel{sec:compute-unit}{2.8}
\newlabel{sec:compute-universe}{2.10}
\newlabel{sec:concluding-remarks}{4.5}
\newlabel{sec:connectivity}{7.5}
\newlabel{sec:conn-susp}{8.2}
\newlabel{sec:constr-cauchy-reals}{11.3.1}
\newlabel{sec:contractibility}{3.11}
\newlabel{sec:contrf}{4.4}
\newlabel{sec:coproduct-types}{1.7}
\newlabel{sec:cumulative-hierarchy}{10.5}
\newlabel{sec:dagger-categories}{9.7}
\newlabel{sec:dedekind-reals}{11.2}
\newlabel{sec:dependent-paths}{6.2}
\newlabel{sec:disequality}{1.12.3}
\newlabel{sec:equality}{2.1}
\newlabel{sec:equality-of-structures}{2.14}
\newlabel{sec:equivalences}{9.4}
\newlabel{sec:equiv-closures}{4.7}
\newlabel{sec:fiberwise-equivalences}{4.7}
\newlabel{sec:fib-over-pushout}{8.5.1}
\newlabel{sec:fibrations}{2.3}
\newlabel{sec:field-rati-numb}{11.1}
\newlabel{sec:finite-product-types}{1.5}
\newlabel{sec:flattening}{6.12}
\newlabel{sec:formal-prelim}{A}
\newlabel{sec:free-algebras}{6.11}
\newlabel{sec:freudenthal}{8.6}
\newlabel{sec:function-types}{1.2}
\newlabel{sec:functors}{2.2}
\newlabel{sec:general-encode-decode}{8.9}
\newlabel{sec:generalizations}{5.7}
\newlabel{sec:hae}{4.2}
\newlabel{sec:hedberg}{7.2}
\newlabel{sec:hittruncations}{6.9}
\newlabel{sec:hopf}{8.5}
\newlabel{sec:hott-features}{A.3}
\newlabel{sec:htpy-inductive}{5.5}
\newlabel{sec:hubs-spokes}{6.7}
\newlabel{sec:identity-systems}{5.8}
\newlabel{sec:identity-types}{1.12}
\newlabel{sec:image}{10.1.2}
\newlabel{sec:image-factorization}{7.6}
\newlabel{sec:inductive-types}{1.9}
\newlabel{sec:induct-recurs-cauchy}{11.3.2}
\newlabel{sec:initial-alg}{5.4}
\newlabel{sec:interval}{6.3}
\newlabel{sec:intro-hits}{6.1}
\newlabel{sec:intuitionism}{3.4}
\newlabel{sec:long-exact-sequence-homotopy-groups}{8.4}
\newlabel{sec:modalities}{7.7}
\newlabel{sec:mono-surj}{4.6}
\newlabel{sec:more-formal-pi}{A.2.4}
\newlabel{sec:more-formal-sigma}{A.2.5}
\newlabel{sec:moreresults}{8.10}
\newlabel{sec:naive-vankampen}{8.7.1}
\newlabel{sec:naturality}{6.13}
\newlabel{sec:n-types}{7.1}
\newlabel{sec:object-classification}{4.8}
\newlabel{sec:ordinals}{10.3}
\newlabel{sec:pat}{1.11}
\newlabel{sec:pattern-matching}{1.10}
\newlabel{sec:pi1s1-classical-proof}{8.1.2}
\newlabel{sec:pi1s1-idsys}{8.1.6}
\newlabel{sec:pi1s1-initial-thoughts}{8.1.1}
\newlabel{sec:pi1-s1-intro}{8.1}
\newlabel{sec:pi1s1-universal-cover}{8.1.3}
\newlabel{sec:pik-le-n}{8.3}
\newlabel{sec:pi-types}{1.4}
\newlabel{sec:piw-pretopos}{10.1}
\newlabel{sec:pushouts}{7.4}
\newlabel{sec:quasi-inverses}{4.1}
\newlabel{sec:RD-cauchy-complete}{11.2.2}
\newlabel{sec:RD-dedekind-complete}{11.2.3}
\newlabel{sec:rezk}{9.9}
\newlabel{sec:set-quotients}{6.10}
\newlabel{sec:sigma-types}{1.6}
\newlabel{sec:sip}{9.8}
\newlabel{sec:strict-categories}{9.6}
\newlabel{sec:strictly-positive}{5.6}
\newlabel{sec:surreals}{11.6}
\newlabel{sec:suspension}{6.5}
\newlabel{sec:syntax-informally}{A.1}
\newlabel{sec:syntax-more-formally}{A.2}
\newlabel{sec:transfors}{9.2}
\newlabel{sec:truncations}{7.3}
\newlabel{sec:type-booleans}{1.8}
\newlabel{sec:types-vs-sets}{1.1}
\newlabel{sec:unique-choice}{3.9}
\newlabel{sec:univalence-implies-funext}{4.9}
\newlabel{sec:universal-properties}{2.15}
\newlabel{sec:universes}{1.3}
\newlabel{sec:van-kampen}{8.7}
\newlabel{sec:wellorderings}{10.4}
\newlabel{sec:whitehead}{8.8}
\newlabel{sec:w-types}{5.3}
\newlabel{sec:yoneda}{9.5}
\newlabel{subsec:emacinsets}{10.1.5}
\newlabel{subsec:general-remarks}{A.4}
\newlabel{subsec:hprops}{3.3}
\newlabel{subsec:limits-sets}{10.1.1}
\newlabel{subsec:logic-hprop}{3.6}
\newlabel{subsec:pat?}{3.2}
\newlabel{subsec:pi1s1-encode-decode}{8.1.4}
\newlabel{subsec:pi1s1-homotopy-theory}{8.1.5}
\newlabel{subsec:piw}{10.1.4}
\newlabel{subsec:prop-subsets}{3.5}
\newlabel{subsec:prop-trunc}{3.7}
\newlabel{subsec:quotients}{10.1.3}
\newlabel{subsec:when-trunc}{3.10}
\newlabel{tab:homotopy-groups-of-spheres}{8.1}
\newlabel{tab:pov}{1}
\newlabel{tab:theorems}{8.2}
\newlabel{thm:1surj_to_surj_to_pem}{10.1.14}
\newlabel{thm:ac-epis-split}{3.8.2}
\newlabel{thm:allbool-trueorfalse}{1.8.1}
\newlabel{thm:ap2}{6.4.4}
\newlabel{thm:apd2}{6.4.6}
\newlabel{thm:apd-const}{2.3.8}
\newlabel{thm:ap-prod}{2.6.5}
\newlabel{thm:ap-sigma-rect-path-pair}{6.12.7}
\newlabel{thm:ap-transport}{2.3.11}
\newlabel{thm:Cauchy-reals-are-a-set}{11.3.9}
\newlabel{thm:conemap-funct}{7.4.10}
\newlabel{thm:connected-pointed}{7.5.11}
\newlabel{thm:conn-pik}{8.4.8}
\newlabel{thm:conn-trunc-variable-ind}{8.6.1}
\newlabel{thm:contr-contr}{3.11.5}
\newlabel{thm:contr-forall}{3.11.6}
\newlabel{thm:contr-hae}{4.2.6}
\newlabel{thm:contr-hprop}{4.4.4}
\newlabel{thm:contr-paths}{3.11.8}
\newlabel{thm:contr-unit}{3.11.3}
\newlabel{thm:conversion-preserves-typing}{A.4.1}
\newlabel{thm:covering-spaces}{8.10.4}
\newlabel{thm:dpath-arrow}{2.9.6}
\newlabel{thm:dpath-forall}{2.9.7}
\newlabel{thm:dpath-path}{2.11.5}
\newlabel{thm:EckmannHilton}{2.1.6}
\newlabel{thm:encode-total-equiv}{8.1.13}
\newlabel{thm:equiv-biinv-isequiv}{4.3.3}
\newlabel{thm:equiv-compose-equiv}{4.2.8}
\newlabel{thm:equiv-contr-hae}{4.4.5}
\newlabel{thm:equiv-eqrel}{2.4.12}
\newlabel{thm:equiv-induction}{5.8.5}
\newlabel{thm:equiv-inhabcod}{4.4.6}
\newlabel{thm:equiv-iso-adj}{4.2.3}
\newlabel{thm:eta-sigma}{2.7.3}
\newlabel{thm:ETCS}{10.1.15}
\newlabel{thm:fiber-of-a-fibration}{4.8.1}
\newlabel{thm:fiber-of-the-fiber}{8.4.4}
\newlabel{thm:flattening}{6.12.2}
\newlabel{thm:flattening-rect}{6.12.4}
\newlabel{thm:flattening-rectnd}{6.12.5}
\newlabel{thm:flattening-rectnd-beta-ppt}{6.12.8}
\newlabel{thm:freegroup-nonset}{6.11.8}
\newlabel{thm:free-monoid}{6.11.5}
\newlabel{thm:freudcode}{8.6.5}
\newlabel{thm:freudenthal}{8.6.4}
\newlabel{thm:freudlemma}{8.6.10}
\newlabel{thm:hae-hprop}{4.2.13}
\newlabel{thm:hedberg}{7.2.5}
\newlabel{thm:hlevel-cumulative}{7.1.7}
\newlabel{thm:hlevel-loops}{7.2.7}
\newlabel{thm:hleveln-of-hlevelSn}{7.1.11}
\newlabel{thm:hlevel-prod}{7.1.9}
\newlabel{thm:h-level-retracts}{7.1.4}
\newlabel{thm:homotopy-groups}{6.11.4}
\newlabel{thm:h-set-refrel-in-paths-sets}{7.2.2}
\newlabel{thm:h-set-uip-K}{7.2.1}
\newlabel{thm:htpy-induction}{5.8.6}
\newlabel{thm:identity-systems}{5.8.2}
\newlabel{thm:inhabprop-eqvunit}{3.3.2}
\newlabel{thm:injsurj}{10.2.9}
\newlabel{thm:interval-funext}{6.3.2}
\newlabel{thm:isaprop-isofhlevel}{7.1.10}
\newlabel{thm:isntype-mono}{7.1.6}
\newlabel{thm:isprop-biinv}{4.3.2}
\newlabel{thm:isprop-forall}{3.6.2}
\newlabel{thm:isprop-iscontr}{3.11.4}
\newlabel{thm:isprop-isprop}{3.3.5}
\newlabel{thm:isprop-isset}{3.3.5}
\newlabel{thm:isset-forall}{3.1.6}
\newlabel{thm:isset-is1type}{3.1.8}
\newlabel{thm:isset-prod}{3.1.5}
\newlabel{thm:kbar}{8.7.9}
\newlabel{thm:lequiv-contr-hae}{4.4.3}
\newlabel{thm:les}{8.4.6}
\newlabel{thm:loop-nontrivial}{6.4.1}
\newlabel{thm:looptothe}{6.10.13}
\newlabel{thm:minusoneconn-surjective}{7.5.2}
\newlabel{thm:ML-identity-systems}{5.8.4}
\newlabel{thm:modal-char}{7.7.4}
\newlabel{thm:modal-mono}{7.6.2}
\newlabel{thm:mono}{10.1.1}
\newlabel{thm:mono-surj-equiv}{4.6.3}
\newlabel{thm:naive-van-kampen}{8.7.4}
\newlabel{thm:nat-hinitial}{5.4.5}
\newlabel{thm:nat-set}{3.1.4}
\newlabel{thm:nat-uniq}{5.1.1}
\newlabel{thm:nat-wf}{10.3.5}
\newlabel{thm:nconn-to-ntype-const}{7.5.9}
\newlabel{thm:nobject-classifier-appetizer}{4.8.3}
\newlabel{thm:NO-encode-decode}{11.6.16}
\newlabel{thm:no-higher-ac}{3.8.5}
\newlabel{thm:NO-refl-opt}{11.6.4}
\newlabel{thm:NO-set}{11.6.5}
\newlabel{thm:NO-simplicity}{11.6.2}
\newlabel{thm:not-dneg}{3.2.2}
\newlabel{thm:not-lem}{3.2.7}
\newlabel{thm:NO-unstrict-transitive}{11.6.17}
\newlabel{thm:ntype-nloop}{7.2.9}
\newlabel{thm:ntypes-sigma}{7.1.8}
\newlabel{thm:object-classifier}{4.8.4}
\newlabel{thm:omg}{2.1.4}
\newlabel{thm:omit-contr}{3.11.9}
\newlabel{thm:ordord}{10.3.20}
\newlabel{thm:ordsucc}{10.3.21}
\newlabel{thm:ordunion}{10.3.22}
\newlabel{thm:orth-fact}{7.6.6}
\newlabel{thm:path-coprod}{2.12.5}
\newlabel{thm:path-lifting}{2.3.2}
\newlabel{thm:path-nat}{2.13.1}
\newlabel{thm:path-prod}{2.6.2}
\newlabel{thm:path-sigma}{2.7.2}
\newlabel{thm:paths-respects-equiv}{2.11.1}
\newlabel{thm:path-subset}{3.5.1}
\newlabel{thm:path-truncation}{7.3.12}
\newlabel{thm:path-unit}{2.8.1}
\newlabel{thm:pi1s1-decode}{8.1.6}
\newlabel{thm:pik-conn}{8.8.5}
\newlabel{thm:prod-ump}{2.15.2}
\newlabel{thm:prod-umpd}{2.15.5}
\newlabel{thm:prop-minusonetype}{3.11.10}
\newlabel{thm:prop-set}{3.3.4}
\newlabel{thm:pushout-ump}{6.8.2}
\newlabel{thm:quotient-surjective}{6.10.2}
\newlabel{thm:quotient-ump}{6.10.3}
\newlabel{thm:RC-le-grow}{11.3.42}
\newlabel{thm:RC-lt-open}{11.3.43}
\newlabel{thm:RC-sim-characterization}{11.3.32}
\newlabel{thm:RC-sim-lim}{11.3.36}
\newlabel{thm:RC-sim-lim-term}{11.3.37}
\newlabel{thm:RCsim-symmetric}{11.3.12}
\newlabel{thm:refl-over-ntype-base}{7.3.10}
\newlabel{thm:reflsubunv-forall}{7.7.2}
\newlabel{thm:retract-contr}{3.11.7}
\newlabel{thm:retract-equiv}{4.7.4}
\newlabel{thm:retraction-quotient}{6.10.10}
\newlabel{thm:S1-autohtpy}{6.4.2}
\newlabel{thm:S1rec}{6.2.5}
\newlabel{thm:S1ump}{6.2.9}
\newlabel{thm:ses}{8.4.7}
\newlabel{thm:set-pushout}{6.9.3}
\newlabel{thm:set_regular}{10.1.5}
\newlabel{thm:settopos}{10.1.12}
\newlabel{thm:sign-induction}{6.10.12}
\newlabel{thm:sip}{9.8.2}
\newlabel{thm:stable-images}{7.6.9}
\newlabel{thm:strong-normalization}{A.4.2}
\newlabel{thm:suspbool}{6.5.1}
\newlabel{thm:suspension-increases-connectedness}{8.2.1}
\newlabel{thm:total-fiber-equiv}{4.7.7}
\newlabel{thm:total-space-of-the-fibers}{4.8.2}
\newlabel{thm:transport2}{6.4.5}
\newlabel{thm:transport-compose}{2.3.10}
\newlabel{thm:transport-concat}{2.3.9}
\newlabel{thm:transportequiv}{2.4.9}
\newlabel{thm:transport-is-ap}{2.10.5}
\newlabel{thm:transport-is-given}{6.12.1}
\newlabel{thm:transport-path}{2.11.3}
\newlabel{thm:transport-path2}{2.11.4}
\newlabel{thm:trans-prod}{2.6.4}
\newlabel{thm:trans-trivial}{2.3.5}
\newlabel{thm:trunc0-ind}{6.9.1}
\newlabel{thm:trunc0-lump}{6.9.2}
\newlabel{thm:trunc-htpy}{7.3.5}
\newlabel{thm:trunc-in-truncated-sigma}{7.3.9}
\newlabel{thm:truncn-ind}{7.3.2}
\newlabel{thm:trunc-reflective}{7.3.3}
\newlabel{thm:ttac}{2.15.7}
\newlabel{thm:two-out-of-three}{4.7.1}
\newlabel{thm:type-is-not-a-set}{3.1.9}
\newlabel{thm:van-Kampen}{8.7.12}
\newlabel{thm:VisCST}{10.5.8}
\newlabel{thm:wedge-connectivity}{8.6.2}
\newlabel{thm:wellorder}{10.4.3}
\newlabel{thm:wfcat}{10.3.15}
\newlabel{thm:wfmin}{10.3.8}
\newlabel{thm:wfrec}{10.3.7}
\newlabel{thm:w-hinit}{5.4.7}
\newlabel{thm:whitehead0}{8.8.1}
\newlabel{thm:whitehead1}{8.8.2}
\newlabel{thm:whitehead-contr}{8.8.4}
\newlabel{thm:whiteheadn}{8.8.3}
\newlabel{thm:wop}{10.4.4}
\newlabel{thm:wtype-wf}{10.3.6}
\newlabel{thm:w-uniq}{5.3.1}
\newlabel{thm:zfc}{10.5.11}
\newlabel{transport-Sigma}{2.7.4}
\newlabel{UA-eqv-hom-eqv}{4.9.2}
\newlabel{uatowfe}{4.9.4}
\newlabel{weakfunext}{4.9.1}
\newlabel{wfetofe}{4.9.5}
\newlabel{when-reals-coincide}{11.4.3}
\newlabel{Z-quotient-by-canonical-representatives}{6.10.11}