symbols.tex

\phantomsection % black magic to get TOC to point to correct page
\markboth{}{\textsc{Index of symbols}}
\addcontentsline{toc}{part}{Index of symbols}
\chapter*{Index of symbols}

% Shorthand for \pageref, we have lots of these.
\newcommand{\pg}[1]{p.~\pageref{#1}}
% In the next macro whitespace matters, so be careful
\newcommand{\symbolindex}[2]{\hbox{\makebox[0.2\textwidth][s]{#1\hfill}\hspace*{2.5em}\parbox[t]{0.65\textwidth}{#2\hfill}}\\[1.5pt]}

% The entries in this table are sorted "alphabetically" whatever that means.

{\OPTindexfont % Set same font size as for the index

% MAKE SURE THERE ARE NO EMPTY LINES, OR ELSE WE GET A PARAGRAPH BREAK.
% ALSO, DO NOT INSERT ANY WHITESPACE AT THE BEGINNING OF ARGUMENTS OF \symbolindex
\noindent
%%%%%%%%%% Equalities %%%%%%%%%%
\symbolindex{$x \defeq a$	}{definition, \pg{defn:defeq}}
\symbolindex{$a \jdeq b$	}{judgmental equality, \pg{defn:judgmental-equality}}
\symbolindex{$a =_A b$	}{identity type, \pg{sec:identity-types}}
\symbolindex{$a = b$	}{identity type, \pg{sec:identity-types}}
\symbolindex{$x \defid b$	}{propositional equality by definition, \pg{rmk:defid}}
\symbolindex{$\idtypevar{A}(a,b)$	}{identity type, \pg{sec:identity-types}}
\symbolindex{$\dpath{P}{p}{a}{b}$	}{dependent path type, \pg{eq:dpath}}
\symbolindex{$a \neq b$	}{disequality, \pg{sec:disequality}}
%%%%%%%%%% Stuff that's hard to alphabetize %%%%%%%%%%
\symbolindex{$\refl{x}$	}{reflexivity path at $x$, \pg{sec:identity-types}}
\symbolindex{$\opp{p}$	}{path reversal, \pg{lem:opp}}
\symbolindex{$p\ct q$	}{path concatenation, \pg{lem:concat}}
\symbolindex{$p\leftwhisker r$	}{left whiskering, \pg{thm:EckmannHilton}}
\symbolindex{$r\rightwhisker q$	}{right whiskering, \pg{thm:EckmannHilton}}
\symbolindex{$r\hct s$	}{horizontal concatenation of 2-paths, \pg{thm:EckmannHilton}}
\symbolindex{$g\circ f$	}{composite of functions, \pg{ex:composition}}
\symbolindex{$g\circ f$	}{composite of morphisms in a precategory, \pg{ct:precategory}}
\symbolindex{$\inv{f}$	}{quasi-inverse of an equivalence, \pg{thm:equiv-eqrel}}
\symbolindex{$\inv{f}$	}{inverse of an isomorphism in a precategory, \pg{ct:inv}}
%%%%%%%%%% Numbers etc. %%%%%%%%%%
\symbolindex{$\emptyt$	}{empty type, \pg{sec:coproduct-types}}
\symbolindex{$\unit$	}{unit type, \pg{sec:finite-product-types}}
\symbolindex{$\ttt$	}{canonical inhabitant of $\unit$, \pg{sec:finite-product-types}}
\symbolindex{$\bool$	}{type of booleans, \pg{sec:type-booleans}}
\symbolindex{$\btrue$, $\bfalse$	}{constructors of $\bool$, \pg{sec:type-booleans}}
\symbolindex{$\izero$, $\ione$	}{point-constructors of the interval $\interval$, \pg{sec:interval}}
%%%%%%%%%% A %%%%%%%%%%
\symbolindex{$\choice{}$	}{axiom of choice, \pg{eq:ac}}
\symbolindex{$\choice{\infty}$	}{``type-theoretic axiom of choice'', \pg{thm:ttac}}
\symbolindex{$\acc(a)$	}{accessibility predicate, \pg{defn:accessibility}}
\symbolindex{$P \land Q$	}{logical conjunction (``and''), \pg{defn:logical-notation}}
\symbolindex{$\apfunc{f}(p)$ or $\ap{f}{p}$	}{application of $f:A\to B$ to $p:\id[A]xy$, \pg{lem:map}}
\symbolindex{$\apd{f}{p}$	}{application of $f:\prd{a:A} B(a)$ to $p:\id[A]xy$, \pg{lem:mapdep}}
% This is not currently a distinctive notation that someone would look up
% $\aptwo{f}{p}$ & two-dimensional $\apfunc{}$, \pg{thm:ap2}
% \\
\symbolindex{$\apdtwo{f}{p}$	}{two-dimensional dependent $\apfunc{}$, \pg{thm:apd2}}
\symbolindex{$x\apart y$	}{apartness of real numbers, \pg{apart}}
%%%%%%%%%% B %%%%%%%%%%
\symbolindex{$\base$	}{basepoint of $\Sn^1$, \pg{sec:intro-hits}}
\symbolindex{$\base$            }{basepoint of $\Sn^2$, \pg{s2a} and \pg{s2b}}
\symbolindex{$\biinv(f)$        }{proposition that $f$ is bi-invertible, \pg{defn:biinv}}
\symbolindex{$x \bisim y$       }{bisimulation, \pg{def:bisimulation}}
\symbolindex{$\blank$           }{blank used for implicit $\lambda$-abstractions, \pg{blank}}
%%%%%%%%%% C %%%%%%%%%%
\symbolindex{$\CAP$             }{type of Cauchy approximations, \pg{cauchy-approximations}}
\symbolindex{$\card$            }{type of cardinal numbers, \pg{defn:card}}
\symbolindex{$\modal A$         }{reflector or modality applied to $A$, \pg{defn:reflective-subuniverse} and \pg{defn:modality}}
\symbolindex{$\cocone{X}{Y}$    }{type of cocones, \pg{defn:cocone}}
% Not used
%\symbolindex{
%  \cone{X}{Y}$
%}{
%  type of cones
%}
\symbolindex{$\code$            }{family of codes for paths, \pg{sec:compute-coprod}, \pg{S1-universal-cover}, \pg{sec:general-encode-decode}}
\symbolindex{$A \setminus B$    }{subset complement, \pg{complement}}
\symbolindex{$\cons(x,\ell)$    }{concatenation constructor for lists, \pg{lst} and \pg{lst-freemonoid}}
\symbolindex{$\contr_x$         }{path to the center of contraction, \pg{defn:contractible}}
\symbolindex{$\mathcal{F}\cover\pairr{J, \mathcal{G}}$          }{inductive cover, \pg{defn:inductive-cover}}
\symbolindex{$\dcut(L,U)$       }{the property of being a Dedekind cut, \pg{defn:dedekind-reals}}
\symbolindex{$\surr{L}{R}$      }{cut defining a surreal number, \pg{surreal-cut}}
%%%%%%%%%% D %%%%%%%%%%
\symbolindex{$\dgr{X}$          }{morphism reversal in a $\dagger$-category, \pg{sec:dagger-categories}}
\symbolindex{$\decode$          }{decoding function for paths, \pg{sec:compute-coprod}, \pg{S1-universal-cover}, \pg{sec:general-encode-decode}}
%%%%%%%%%% E %%%%%%%%%%
\symbolindex{$\encode$	}{encoding function for paths, \pg{sec:compute-coprod}, \pg{S1-universal-cover}, \pg{sec:general-encode-decode}}
\symbolindex{$\mreturn^\modal_A$ or $\mreturn_A$	}{the function $A\to\modal A$, \pg{defn:reflective-subuniverse} and \pg{defn:modality}}
\symbolindex{$A \epi B$	}{epimorphism or surjection}
\symbolindex{$\noeq(x,y)$	}{path-constructor of the surreals, \pg{defn:surreals}}
\symbolindex{$\rceq(u,v)$	}{path-constructor of the Cauchy reals, \pg{defn:cauchy-reals}}
\symbolindex{$a \eqr b$	}{an equivalence relation, \pg{equivalencerelation}}
\symbolindex{$\eqv{X}{Y}$	}{type of equivalences, \pg{eq:eqv}}
\symbolindex{$\texteqv{X}{Y}$	}{type of equivalences (same as $\eqv{X}{Y}$)}
\symbolindex{$\cteqv{A}{B}$	}{type of equivalences of categories, \pg{ct:equiv}}
\symbolindex{$P \Leftrightarrow Q$	}{logical equivalence, \pg{defn:logical-notation}}
\symbolindex{$\exis{x:A} B(x)$	}{logical notation for mere existential, \pg{defn:logical-notation}}
\symbolindex{$\extend f$	}{extension of $f:A\to B$ along $\eta_A$, \pg{extend}}
%%%%%%%%%% F %%%%%%%%%%
\symbolindex{$\bot$	}{logical falsity, \pg{defn:logical-notation}}
\symbolindex{$\hfib{f}{b}$	}{fiber of $f:A\to B$ at $b:B$, \pg{defn:homotopy-fiber}}
\symbolindex{$\Fin(n)$  }{standard finite type, \pg{fin}}
\symbolindex{$\fall{x:A} B(x)$	}{logical notation for dependent function type, \pg{defn:logical-notation}}
\symbolindex{$\funext$	}{function extensionality, \pg{axiom:funext}}
\symbolindex{$A\to B$	}{function type, \pg{sec:function-types}}
%%%%%%%%%% G %%%%%%%%%%
\symbolindex{$\glue$	}{path constructor of $A \sqcup^C B$, \pg{sec:colimits}}
%%%%%%%%%% H %%%%%%%%%%
\symbolindex{$\happly$	}{function making a path of functions into a homotopy, \pg{eq:happly}}
\symbolindex{$\hom_A(a,b)$	}{hom-set in a precategory, \pg{ct:precategory}}
\symbolindex{$f \htpy g$	}{homotopy between functions, \pg{defn:homotopy}}
%%%%%%%%%% I %%%%%%%%%%
\symbolindex{$\interval$	}{the interval type, \pg{sec:interval}}
\symbolindex{$\idfunc[A]$	}{the identity function of $A$, \pg{idfunc}}
\symbolindex{$1_a$	}{identity morphism in a precategory, \pg{ct:precategory}}
\symbolindex{$\idtoeqv$	}{function $(A=B)\to(\eqv A B)$ which univalence inverts, \pg{eq:uidtoeqv}}
\symbolindex{$\idtoiso$	}{function $(a=b) \to (a\cong b)$ in a precategory, \pg{ct:idtoiso}}
\symbolindex{$\im(f)$	}{image of map $f$, \pg{defn:modal-image}}
\symbolindex{$\im_n(f)$	}{$n$-image of map $f$, \pg{defn:modal-image}}
\symbolindex{$P \Rightarrow Q$	}{logical implication (``implies''), \pg{defn:logical-notation}}
\symbolindex{$a \in P$	}{membership in a subset or subtype, \pg{membership}}
\symbolindex{$x\in v$	}{membership in the cumulative hierarchy, \pg{V-membership}}
\symbolindex{$x\bin v$	}{resized membership, \pg{resized-membership}}
\symbolindex{$\ind{\emptyt}$	}{induction for ${\emptyt}$, \pg{defn:induction-emptyt},}
\symbolindex{$\ind{\unit}$	}{induction for ${\unit}$, \pg{defn:induction-unit},}
\symbolindex{$\ind{\bool}$	}{induction for ${\bool}$, \pg{defn:induction-bool},}
\symbolindex{$\ind{\nat}$	}{induction for ${\nat}$, \pg{defn:induction-nat}, and}
\symbolindex{$\indid{A}$	}{path induction for $=_A$, \pg{defn:induction-ML-id},}
\symbolindex{$\indidb{A}$	}{based path induction for $=_A$, \pg{defn:induction-PM-id},}
\symbolindex{$\ind{A \times B}$	}{induction for ${A \times B}$, \pg{defn:induction-times},}
\symbolindex{$\ind{\sm{x:A} B(x)}$	}{induction for ${\sm{x:A} B}$, \pg{defn:induction-sm},}
\symbolindex{$\ind{A + B}$	}{induction for ${A + B}$, \pg{defn:induction-plus},}
\symbolindex{$\ind{\wtype{x:A} B(x)}$	}{induction for ${\wtype{x:A} B}$, \pg{defn:induction-wtype}}
\symbolindex{$\ordsl{A}{a}$	}{initial segment of an ordinal, \pg{initial-segment}}
\symbolindex{$\inj(A,B)$	}{type of injections, \pg{inj}}
\symbolindex{$\inl$	}{first injection into a coproduct, \pg{sec:coproduct-types}}
\symbolindex{$\inr$	}{second injection into a coproduct, \pg{sec:coproduct-types}}
\symbolindex{$A \cap B$	}{intersection of subsets, \pg{intersection}, classes, \pg{class-intersection}, or intervals, \pg{interval-intersection}}
\symbolindex{$\iscontr(A)$	}{proposition that $A$ is contractible, \pg{defn:contractible}}
\symbolindex{$\isequiv(f)$	}{proposition that $f$ is an equivalence, \pg{basics-isequiv}, \pg{cha:equivalences}, and \pg{sec:concluding-remarks}}
\symbolindex{$\ishae(f)$	}{proposition that $f$ is a half-adjoint equivalence, \pg{defn:ishae}}
\symbolindex{$a\cong b$	}{type of isomorphisms in a (pre)category, \pg{ct:isomorphism}}
\symbolindex{$A\cong B$	}{type of isomorphisms between precategories, \pg{ct:isocat}}
\symbolindex{$a\unitaryiso b$	}{type of unitary isomorphisms, \pg{ct:unitary}}
\symbolindex{$\isotoid$	}{inverse of $\idtoiso$ in a category, \pg{isotoid}}
\symbolindex{$\istype{n}(X)$	}{proposition that $X$ is an $n$-type, \pg{def:hlevel}}
\symbolindex{$\isprop(A)$	}{proposition that $A$ is a mere proposition, \pg{defn:isprop}}
\symbolindex{$\isset(A)$	}{proposition that $A$ is a set, \pg{defn:set}}
%%%%%%%%%% J %%%%%%%%%%
\symbolindex{$A*B$	}{join of $A$ and $B$, \pg{join}}
%%%%%%%%%% K %%%%%%%%%%
\symbolindex{$\ker(f)$	}{kernel of a map of pointed sets, \pg{kernel}}
%%%%%%%%%% L %%%%%%%%%%
\symbolindex{$\lam{x} b(x)$	}{$\lambda$-abstraction, \pg{eq:lambda-abstraction}}
\symbolindex{$\lcoh{f}{g}{\eta}$	}{type of left adjoint coherence data, \pg{defn:lcoh-rcoh}}
\symbolindex{$\LEM{}$	}{law of excluded middle, \pg{eq:lem}}
\symbolindex{$\LEM{\infty}$	}{inconsistent propositions-as-types \LEM{}, \pg{thm:not-lem} and \pg{lem-infty}}
\symbolindex{$x < y$	}{strict inequality on natural numbers, \pg{leq-nat}, ordinals, \pg{sec:ordinals}, Cauchy reals, \pg{lt-RC}, surreals, \pg{defn:surreals}, etc.}
\symbolindex{$x \le y$	}{non-strict inequality on natural numbers, \pg{leq-nat}, Cauchy reals, \pg{leq-RC}, surreals, \pg{defn:surreals}, etc.}
\symbolindex{$\preceq$, $\prec$	}{recursive versions of $\le$ and $<$ for surreals, \pg{defn:No-codes}}
\symbolindex{$\ble$, $\blt$, $\bble$, $\bblt$	}{orderings on codomain of $\NO$-recursion, \pg{NO-recursion}}
\symbolindex{$\rclim(x)$	}{limit of a Cauchy approximation, \pg{defn:cauchy-reals}}
\symbolindex{$\linv(f)$	}{type of left inverses to $f$, \pg{defn:linv-rinv}}
\symbolindex{$\lst{X}$	}{type of lists of elements of $X$, \pg{lst} and \pg{lst-freemonoid}}
\symbolindex{$\lloop$	}{path-constructor of $\Sn^1$, \pg{sec:intro-hits}}
%%%%%%%%%% M %%%%%%%%%%
\symbolindex{$\Map_*(A,B)$	}{type of based maps, \pg{based-maps}}
\symbolindex{$x\mapsto b$	}{alternative notation for $\lambda$-abstraction, \pg{mapsto}}
\symbolindex{$\max(x,y)$	}{maximum in some ordering, e.g.\ \pg{ordered-field} and \pg{leq-RC}}
\symbolindex{$\merid(a)$	}{meridian of $\susp A$ at $a:A$, \pg{sec:suspension}}
\symbolindex{$\min(x,y)$	}{minimum in some ordering, e.g.\ \pg{ordered-field} and \pg{leq-RC}}
\symbolindex{$A \mono B$	}{monomorphism or embedding}
%%%%%%%%%% N %%%%%%%%%%
\symbolindex{$\N$	}{type of natural numbers, \pg{sec:inductive-types}}
\symbolindex{$\north$	}{north pole of $\susp A$, \pg{sec:suspension}}
\symbolindex{$\natw$, $\zerow$, $\sucw$	}{natural numbers encoded as a $W$-type, \pg{natw}}
\symbolindex{$\nalg$	}{type of $\nat$-algebras, \pg{defn:nalg}}
\symbolindex{$\nhom(C,D)$	}{type of $\nat$-homomorphisms, \pg{defn:nhom}}
\symbolindex{$\nil$	}{empty list, \pg{lst} and \pg{lst-freemonoid}}
\symbolindex{$\NO$	}{type of surreal numbers, \pg{defn:surreals}}
\symbolindex{$\neg P$	}{logical negation (``not''), \pg{defn:logical-notation}}
\symbolindex{$\typele{n}$, $\typeleU{n}$	}{universe of $n$-types, \pg{universe-of-ntypes}}
%%%%%%%%%% O %%%%%%%%%%
\symbolindex{$\Omega(A,a)$, $\Omega A$		}{loop space of a pointed type, \pg{def:loopspace}}
\symbolindex{$\Omega^k(A,a)$, $\Omega^k A$		}{iterated loop space, \pg{def:loopspace}}
\symbolindex{$A\op$	}{opposite precategory, \pg{ct:opposite-category}}
\symbolindex{$P \lor Q$	}{logical disjunction (``or''), \pg{defn:logical-notation}}
\symbolindex{$\ord$	}{type of ordinal numbers, \pg{ord}}
%%%%%%%%%% P %%%%%%%%%%
\symbolindex{$\pairr{a,b}$	}{(dependent) pair, \pg{sec:finite-product-types} and \pg{defn:dependent-pair}}
\symbolindex{$\pairpath$	}{constructor for $=_{A \times B}$, \pg{defn:pairpath}}
\symbolindex{$\pi_n(A)$	}{$n^{\mathrm{th}}$ homotopy group of $A$, \pg{thm:homotopy-groups} and \pg{def-of-homotopy-groups}}
\symbolindex{$\power A$	}{power set, \pg{powerset}}
\symbolindex{$\powerp A$	}{merely-inhabited power set, \pg{inhabited-powerset}}
\symbolindex{$\Zpred$	}{predecessor function $\Z\to\Z$, \pg{subsec:pi1s1-encode-decode}}
\symbolindex{$A\times B$	}{cartesian product type, \pg{sec:finite-product-types}}
\symbolindex{$\prd{x:A} B(x)$	}{dependent function type, \pg{sec:pi-types}}
\symbolindex{$\proj1(t)$	}{the first projection from a pair, \pg{defn:proj} and \pg{defn:dependent-proj1}}
\symbolindex{$\proj2(t)$	}{the second projection from a pair, \pg{defn:proj} and \pg{defn:dependent-proj1}}
\symbolindex{$\prop$, $\propU$	}{universe of mere propositions, \pg{propU}}
\symbolindex{$A \times_C B$	}{pullback of $A$ and $B$ over $C$, \pg{eq:defn-pullback}}
\symbolindex{$A \sqcup^C B$	}{pushout of $A$ and $B$ under $C$, \pg{sec:colimits}}
%%%%%%%%%% Q %%%%%%%%%%
\symbolindex{$\Q$	}{type of rational numbers, \pg{sec:field-rati-numb}}
\symbolindex{$\Qp$	}{type of positive rational numbers, \pg{positive-rationals}}
\symbolindex{$\qinv(f)$	}{type of quasi-inverses to $f$, \pg{qinv}}
\symbolindex{$A/R$	}{quotient of a set by an equivalence relation, \pg{sec:set-quotients}}
\symbolindex{$A\sslash R$	}{alternative definition of quotient, \pg{def:VVquotient}}
%%%%%%%%%% R %%%%%%%%%%
\symbolindex{$\R$	}{type of real numbers (either), \pg{sec:compactness-interval}}
\symbolindex{$\RC$	}{type of Cauchy real numbers, \pg{defn:cauchy-reals}}
\symbolindex{$\RD$	}{type of Dedekind real numbers, \pg{defn:dedekind-reals}}
\symbolindex{$\rcrat(q)$	}{rational number regarded as a Cauchy real, \pg{defn:cauchy-reals}}
\symbolindex{$\rcoh{f}{g}{\epsilon}$	}{type of right adjoint coherence data, \pg{defn:lcoh-rcoh}}
\symbolindex{$\rec{\emptyt}$	}{recursor for ${\emptyt}$, \pg{defn:recursor-emptyt}}
\symbolindex{$\rec{\unit}$	}{recursor for ${\unit}$, \pg{defn:recursor-unit}}
\symbolindex{$\rec{\bool}$	}{recursor for ${\bool}$, \pg{defn:recursor-bool}}
\symbolindex{$\rec{\nat}$	}{recursor for ${\nat}$, \pg{defn:recursor-nat}}
\symbolindex{$\rec{A \times B}$	}{recursor for ${A \times B}$, \pg{defn:recursor-times}}
\symbolindex{$\rec{\sm{x:A} B(x)}$	}{recursor for ${\sm{x:A} B}$, \pg{defn:recursor-sm}}
\symbolindex{$\rec{A + B}$	}{recursor for ${A + B}$, \pg{defn:recursor-plus}}
\symbolindex{$\rec{\wtype{x:A} B(x)}$	}{recursor for ${\wtype{x:A} B}$, \pg{defn:recursor-wtype}}
\symbolindex{$\rinv$	}{type of right inverses to $f$, \pg{defn:linv-rinv}}
%%%%%%%%%% S %%%%%%%%%%
\symbolindex{$\south$	}{south pole of $\susp A$, \pg{sec:suspension}}
\symbolindex{$\Sn^n$	}{$n$-dimensional sphere, \pg{sec:circle}}
\symbolindex{$\seg$	}{path-constructor of the interval $\interval$, \pg{sec:interval}}
\symbolindex{$\set$, $\setU$	}{universe of sets, \pg{setU}}
\symbolindex{$\uset$	}{category of sets, \pg{ct:precatset}}
\symbolindex{$\vset(A,f)$	}{constructor of the cumulative hierarchy, \pg{defn:V}}
\symbolindex{$x\sim_\epsilon y$	}{relation of $\epsilon$-closeness for $\RC$, \pg{defn:cauchy-reals}}
\symbolindex{$x\approx_\epsilon y$	}{recursive version of $\sim_\epsilon$, \pg{defn:RC-approx}}
\symbolindex{$\bsim_\epsilon$ or $\bbsim_\epsilon$	}{closeness relations on codomain of $\RC$-recursion, \pg{RC-recursion}}
\symbolindex{$A\wedge B$	}{smash product of $A$ and $B$, \pg{smash}}
\symbolindex{$\setof{x : A | P(x)}$	}{subset type, \pg{defn:setof}}
\symbolindex{$\setof{ f(x) | P(x)}$	}{image of a subset, \pg{subset-image}}
\symbolindex{$B \subseteq C$	}{containment of subset types, \pg{subset}}
\symbolindex{$(q,r)\subseteq (s,t)$	}{inclusion of intervals, \pg{interval-subset}}
\symbolindex{$\suc$	}{successor function $\N\to\N$, \pg{sec:inductive-types}}
\symbolindex{$\Zsuc$	}{successor function $\Z\to\Z$, \pg{sec:pi1s1-initial-thoughts}}
\symbolindex{$A+B$	}{coproduct type, \pg{sec:coproduct-types}}
\symbolindex{$\sm{x:A} B(x)$	}{dependent pair type, \pg{sec:sigma-types}}
\symbolindex{$\supp(a, f)$	}{constructor for $W$-type, \pg{defn:supp}}
\symbolindex{$\surf$	}{2-path constructor of $\Sn^2$, \pg{s2a} and \pg{s2b}}
\symbolindex{$\susp A$	}{suspension of $A$, \pg{sec:suspension}}
%%%%%%%%%% T %%%%%%%%%%
\symbolindex{$\total{f}$	}{induced map on total spaces, \pg{defn:total-map}}
\symbolindex{$\trans{p}{u}$	}{transport of $u:P(x)$ along $p:x=y$, \pg{lem:transport}}
\symbolindex{$\transfib{P}{p}{u}$	}{transport of $u:P(x)$ along $p:x=y$, \pg{lem:transport}}
\symbolindex{$\transtwo{X}{Y}$	}{two-dimensional transport, \pg{thm:transport2}}
\symbolindex{$\transconst{X}{Y}{Z}$	}{transporting in a constant family, \pg{thm:trans-trivial}}
\symbolindex{$\trunc{n}{A}$	}{$n$-truncation of $A$, \pg{sec:truncations}}
\symbolindex{$\tproj[A]{n}{a}$, $\tproj{n}{a}$	}{image of $a:A$ in $\trunc n A$, \pg{sec:truncations}}
\symbolindex{$\brck{A}$	}{propositional truncation of $A$, \pg{subsec:prop-trunc} and \pg{sec:hittruncations}}
\symbolindex{$\bproj{a}$	}{image of $a:A$ in $\brck A$, \pg{subsec:prop-trunc} and \pg{sec:hittruncations}}
\symbolindex{$\top$	}{logical truth, \pg{defn:logical-notation}}
%%%%%%%%%% U %%%%%%%%%%
\symbolindex{$\nameless$	}{an unnamed object or variable}
\symbolindex{$A \cup B$	}{union of subsets, \pg{union}}
\symbolindex{$\uniq{A\times B}$ }{uniqueness principle for the product $A\times B$, \pg{uniquenessproduct}}
\symbolindex{$\uniq{\unit}$     }{uniqueness principle for $\unit$, \pg{uniquenessunit}}
\symbolindex{$\UU$	}{universe type, \pg{sec:universes}}
\symbolindex{$\modaltype$	}{universe of modal types, \pg{eq:modaltype}}
\symbolindex{$\pointed\type$	}{universe of pointed types, \pg{def:pointedtype}}
\symbolindex{$\ua$	}{inverse to $\idtoeqv$ from univalence, \pg{ua}}
%%%%%%%%%% V %%%%%%%%%%
\symbolindex{$V$	}{cumulative hierarchy, \pg{defn:V}}
%%%%%%%%%% W %%%%%%%%%%
\symbolindex{$\walg(A,B)$	}{type of $w$-algebras, \pg{walg}}
\symbolindex{$\whom_{A,B}(C,D)$	}{type of $\w$-homomorphisms, \pg{whom}}
\symbolindex{$\wtype{x:A} B(x)$	}{$W$-type (inductive type), \pg{sec:w-types}}
\symbolindex{$A\vee B$	}{wedge of $A$ and $B$, \pg{wedge}}
%%%%%%%%%% X %%%%%%%%%%
%%%%%%%%%% Y %%%%%%%%%%
\symbolindex{$\y$	}{Yoneda embedding, \pg{ct:yoneda}}
%%%%%%%%%% Z %%%%%%%%%%
\symbolindex{$\Z$	}{type of integers, \pg{defn-Z}}}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "hott-online"
%%% End: