Quotation style

basics.tex

@@ -159,7 +159,7 @@ \chapter{Homotopy type theory}
 %% (Obviously, the
 %% notation ``$\id[A]{x}{y}$'' has its limitations here.  The style
 %% $\idtype[A]{x}{y}$ is only slightly better in iterations:
-%% $\idtype[{\idtype[{\idtype[A]{x}{y}}]{p}{q}}]{r}{s}$.)
+%% $\idtype[{\idtype[{\idtype[A]{x}{y}}]{p}{q}}]{r}{s}$).
 
 An important difference between homotopy type theory and classical homotopy theory is that homotopy type theory provides a \emph{synthetic}
 \index{synthetic mathematics}%
@@ -203,7 +203,7 @@ \chapter{Homotopy type theory}
 
 The ``conversion rule''~\eqref{eq:Jconv} is less familiar in the context of proof by induction on natural numbers, but there is an analogous notion in the related concept of definition by recursion.
 If a sequence\index{sequence} $(a_n)_{n\in \mathbb{N}}$ is defined by giving $a_0$ and specifying $a_{n+1}$ in terms of $a_n$, then in fact the $0^{\mathrm{th}}$ term of the resulting sequence \emph{is} the given one, and the given recurrence relation relating $a_{n+1}$ to $a_n$ holds for the resulting sequence.
-(This may seem so obvious as to not be worth saying, but if we view a definition by recursion as an algorithm\index{algorithm} for calculating values of a sequence, then it is precisely the process of executing that algorithm.)
+(This may seem so obvious as to not be worth saying, but if we view a definition by recursion as an algorithm\index{algorithm} for calculating values of a sequence, then it is precisely the process of executing that algorithm).
 The rule~\eqref{eq:Jconv} is analogous: it says that if we define an object $f(p)$ for all $p:x=y$ by specifying what the value should be when $p$ is $\refl{x}:x=x$, then the value we specified is in fact the value of $f(\refl{x})$.
 
 This induction principle endows each type with the structure of an $\infty$-groupoid\index{.infinity-groupoid@$\infty$-groupoid}, and each function between two types the structure of an $\infty$-functor\index{.infinity-functor@$\infty$-functor} between two such groupoids.  This is interesting from a mathematical point of view, because it gives a new way to work with
@@ -238,7 +238,7 @@ \section{Types are higher groupoids}
 \[ \prd{A:\UU}{x,y:A} (x= y)\to(y= x). \]
 The proof of \autoref{lem:opp} will consist of constructing an element of this type, i.e.\ deriving the judgment $f:\prd{A:\UU}{x,y:A} (x= y)\to(y= x)$ for some $f$.
 We then introduce the notation $\opp{(\blank)}$ for this element $f$, in which the arguments $A$, $x$, and $y$ are omitted and inferred from context.
-(As remarked in \autoref{sec:types-vs-sets}, the secondary statement ``$\opp{\refl{x}}\jdeq\refl{x}$ for each $x:A$'' should be regarded as a separate judgment.)
+(As remarked in \autoref{sec:types-vs-sets}, the secondary statement ``$\opp{\refl{x}}\jdeq\refl{x}$ for each $x:A$'' should be regarded as a separate judgment).
 
 \begin{proof}[First proof]
   Assume given $A:\UU$, and
@@ -347,7 +347,7 @@ \section{Types are higher groupoids}
 The asymmetrical computation rules can sometimes be convenient when doing formalized mathematics, as they allow the computer to simplify more things automatically.
 However, in informal mathematics, and arguably even in the formalized case, it can be confusing to have a concatenation operation which behaves asymmetrically and to have to remember which side is the ``special'' one.
 Treating both sides symmetrically makes for more robust proofs; this is why we have given the proof that we did.
-(However, this is admittedly a stylistic choice.)
+(However, this is admittedly a stylistic choice).
 
 The table below summarizes the ``equality'', ``homotopical'', and ``higher-groupoid" points of view on what we have done so far.
 \begin{center}
@@ -371,7 +371,7 @@ \section{Types are higher groupoids}
   a &= b & \text{(by $p$)}\\ &= c &\text{(by $q$)} \\ &= d &\text{(by $r$)}.
 \end{align*}
 In either case, the notation indicates construction of the element $(p\ct q)\ct r: (a=d)$.
-(We choose left-associativity for concreteness, although in view of \autoref{thm:omg}\ref{item:omg4} below it makes little difference.)
+(We choose left-associativity for concreteness, although in view of \autoref{thm:omg}\ref{item:omg4} below it makes little difference).
 If it should happen that $b$ and $c$, say, are judgmentally equal, then we may write
 \begin{align*}
   a &= b & \text{(by $p$)}\\ &\jdeq c \\ &= d &\text{(by $r$)}
@@ -383,7 +383,7 @@ \section{Types are higher groupoids}
 
 Now, because of proof-relevance, we can't stop after proving ``symmetry'' and ``transitivity'' of equality: we need to know that these \emph{operations} on equalities are well-behaved.
 (This issue is invisible in set theory, where symmetry and transitivity are mere \emph{properties} of equality, rather than structure on
-paths.)
+paths).
 From the homotopy-theoretic point of view, concatenation and inversion are just the ``first level'' of higher groupoid structure --- we also need coherence\index{coherence} laws on these operations, and analogous operations at higher dimensions.
 For instance, we need to know that concatenation is \emph{associative}, and that inversion provides \emph{inverses} with respect to concatenation.
 
@@ -613,7 +613,7 @@ \section{Types are higher groupoids}
   &\jdeq \opp{\refl{\refl{a}}} \ct \alpha \ct \refl{\refl{a}} \ct \opp{\refl{\refl a}} \ct \beta \ct \refl{\refl{a}}\\
   &= \alpha \ct \beta.
 \end{align*}
-(Recall that $\mathsf{ru}_{\refl{a}} \jdeq \mathsf{lu}_{\refl{a}} \jdeq \refl{\refl{a}}$, by the computation rule for path induction.)
+(Recall that $\mathsf{ru}_{\refl{a}} \jdeq \mathsf{lu}_{\refl{a}} \jdeq \refl{\refl{a}}$, by the computation rule for path induction).
 On the other hand, we can define another horizontal composition analogously by
 \[
 \alpha\hct'\beta\ \defeq\ (p\leftwhisker \beta)\ct (\alpha\rightwhisker s).
@@ -1073,7 +1073,7 @@ \section{Homotopies and equivalences}
 \end{equation}
 is poorly behaved.
 For instance, for a single function $f:A\to B$ there may be multiple unequal inhabitants of~\eqref{eq:qinvtype}.
-(This is closely related to the observation in higher category theory that often one needs to consider \emph{adjoint} equivalences\index{adjoint!equivalence} rather than plain equivalences.)
+(This is closely related to the observation in higher category theory that often one needs to consider \emph{adjoint} equivalences\index{adjoint!equivalence} rather than plain equivalences).
 For this reason, we give~\eqref{eq:qinvtype} the following historically accurate, but slightly de\-rog\-a\-to\-ry-sounding name instead.
 
 \begin{defn}\label{defn:quasi-inverse}
@@ -1678,7 +1678,7 @@ \section{Universes and the univalence axiom}
   \index{identity!function}%
   \index{function!identity}%
   Note that the identity function $\idfunc[\type]:\type\to\type$ may be regarded as a type family indexed by the universe \type; it assigns to each type $X:\type$ the type $X$ itself.
-  (When regarded as a fibration, its total space is the type $\sm{A:\type}A$ of ``pointed types''; see also \autoref{sec:object-classification}.)
+  (When regarded as a fibration, its total space is the type $\sm{A:\type}A$ of ``pointed types''; see also \autoref{sec:object-classification}).
   Thus, given a path $p:A =_\type B$, we have a transport\index{transport} function $\transf{p}:A \to B$.
   We claim that $\transf{p}$ is an equivalence.
   But by induction, it suffices to assume that $p$ is $\refl A$, in which case $\transf{p} \jdeq \idfunc[A]$, which is an equivalence by \autoref{eg:idequiv}.
@@ -1896,12 +1896,12 @@ \section{Coproducts}
 We now consider our first example of a \emph{positive} type former.
 \index{type!positive}\index{positive!type}%
 Again informally, a positive type is one which is ``presented'' by certain constructors, with the universal property of a presentation\index{presentation!of a positive type by its constructors} being expressed by its elimination rule.
-(Categorically speaking, a positive type has a ``mapping out'' universal property, while a negative type has a ``mapping in'' universal property.)
+(Categorically speaking, a positive type has a ``mapping out'' universal property, while a negative type has a ``mapping in'' universal property).
 Because computing with presentations is, in general, an uncomputable problem, for positive types we cannot always expect a straightforward characterization of the identity type.
 However, in many particular cases, a characterization or partial characterization does exist, and can be obtained by the general method that we introduce with this example.
 
 (Technically, our chosen presentation of cartesian products and $\Sigma$-types is also positive.
-However, because these types also admit a negative presentation which differs only slightly, their identity types have a direct characterization that does not require the method to be described here.)
+However, because these types also admit a negative presentation which differs only slightly, their identity types have a direct characterization that does not require the method to be described here).
 
 Consider the coproduct type $A+B$, which is ``presented'' by the injections $\inl:A\to A+B$ and $\inr:B\to A+B$.
 Intuitively, we expect that $A+B$ contains exact copies of $A$ and $B$ disjointly, so that we should have
@@ -2326,7 +2326,7 @@ \section{Universal properties}
 \begin{proof}
   We define the quasi-inverse by sending $(g,h)$ to $\lam{x}(g(x),h(x))$.
   (Technically, we have used the induction principle for the cartesian product $(X\to A)\times (X\to B)$, to reduce to the case of a pair.
-  From now on we will often apply this principle without explicit mention.)
+  From now on we will often apply this principle without explicit mention).
 
   Now given $f:X\to A\times B$, the round-trip composite yields the function
   \begin{equation}
@@ -2394,7 +2394,7 @@ \section{Universal properties}
 \end{itemize}
 Thus, \autoref{thm:ttac} says that not only is the axiom of choice ``true'', its antecedent is actually equivalent to its conclusion.
 (On the other hand, the classical\index{mathematics!classical} mathematician may find that~\eqref{eq:sigma-ump-map} does not carry the usual meaning of the axiom of choice, since we have already specified the values of $g$, and there are no choices left to be made.
-We will return to this point in \autoref{sec:axiom-choice}.)
+We will return to this point in \autoref{sec:axiom-choice}).
 
 The above universal property for pair types is for ``mapping in'', which is familiar from the category-theoretic notion of products.
 However, pair types also have a universal property for ``mapping out'', which may look less familiar.
@@ -2598,14 +2598,14 @@ \section{Universal properties}
 \begin{ex}\label{ex:equality-reflection}
   Suppose we add to type theory the \emph{equality reflection rule} which says that if there is an element $p:x=y$, then in fact $x\jdeq y$.
   Prove that for any $p:x=x$ we have $p\jdeq \refl{x}$.
-  (This implies that every type is a \emph{set} in the sense to be introduced in \autoref{sec:basics-sets}; see \autoref{sec:hedberg}.)
+  (This implies that every type is a \emph{set} in the sense to be introduced in \autoref{sec:basics-sets}; see \autoref{sec:hedberg}).
 \end{ex}
 
 \begin{ex}
   Show that \autoref{thm:transport-is-ap} can be strengthened to
   \[\transfib{B}{p}{{\blank}} =_{B(x)\to B(y)} \idtoeqv(\apfunc{B}(p))\]
   without using function extensionality.
-  (In this and other similar cases, the apparently weaker formulation has been chosen for readability and consistency.)
+  (In this and other similar cases, the apparently weaker formulation has been chosen for readability and consistency).
 \end{ex}
 
 \begin{ex}\label{ex:strong-from-weak-funext}

categories.tex

@@ -230,7 +230,7 @@ \section{Categories and precategories}
   \indexdef{fundamental!pregroupoid}%
   \indexsee{pregroupoid, fundamental}{fundamental pregroupoid}%
   of $X$.
-  (In fact, we have met it already in \autoref{sec:van-kampen}; see also \autoref{ex:rezk-vankampen}.)
+  (In fact, we have met it already in \autoref{sec:van-kampen}; see also \autoref{ex:rezk-vankampen}).
 \end{eg}
 
 \begin{eg}\label{ct:hoprecat}
@@ -446,7 +446,7 @@ \section{Functors and transformations}
 \end{proof}
 
 The equality in \autoref{ct:functor-assoc} is likewise not definitional.
-(Composition of functions is definitionally associative, but the axioms that go into a functor must also be composed, and this breaks definitional associativity.)  For this reason, we need also to know about \emph{coherence}\index{coherence} for associativity.
+(Composition of functions is definitionally associative, but the axioms that go into a functor must also be composed, and this breaks definitional associativity).  For this reason, we need also to know about \emph{coherence}\index{coherence} for associativity.
 
 \begin{lem}\label{ct:pentagon}
   \index{associativity!of functor composition!coherence of}%
@@ -672,7 +672,7 @@ \section{Equivalences}
 This is an important advantage of our category theory over set-based approaches.
 With a purely set-based definition of category, the statement ``every fully faithful and essentially surjective functor is an equivalence of categories'' is equivalent to the axiom of choice \choice{}.
 Here we have it for free, as a category-theoretic version of the principle of unique choice (\autoref{sec:unique-choice}).
-(In fact, this property characterizes categories among precategories; see \autoref{sec:rezk}.)
+(In fact, this property characterizes categories among precategories; see \autoref{sec:rezk}).
 
 On the other hand, the following characterization of equivalences of categories is perhaps even more useful.
 
@@ -773,7 +773,7 @@ \section{Equivalences}
     \circ g\\
     &= g.
   \end{align*}
-  (There are lemmas needed here regarding the compatibility of \idtoiso and whiskering, which we leave it to the reader to state and prove.)
+  (There are lemmas needed here regarding the compatibility of \idtoiso and whiskering, which we leave it to the reader to state and prove).
   Thus, $F_{a,a'}$ is an equivalence, so $F$ is fully faithful; i.e.~\ref{item:ct:ipc1} holds.
 
   Now the composite~\ref{item:ct:ipc1}$\to$\ref{item:ct:ipc2}$\to$\ref{item:ct:ipc1} is equal to the identity since~\ref{item:ct:ipc1} is a mere proposition.
@@ -841,7 +841,7 @@ \section{Equivalences}
   \item identities $\id{\trans {(P_{a,a})} {1_a}}{1_{\trans {P_0} a}}$ and
     \narrowequation{\id{\trans {(P_{a,c})} {gf}}{\trans {(P_{b,c})} g \circ \trans {(P_{a,b})} f}.}
   \end{itemize}
-  (Again, we use the fact that the identity types of hom-sets are mere propositions.)
+  (Again, we use the fact that the identity types of hom-sets are mere propositions).
   However, by univalence, this is equivalent to giving
   \begin{itemize}
   \item an equivalence of types $F_0:\eqv{A_0}{B_0}$,
@@ -1099,7 +1099,7 @@ \section{Strict categories}
   \indexsee{monic}{monomorphism}
   \begin{itemize}
   \item Its objects consist of an object $y:A$ and a monomorphism $m:\hom_A(y,x)$.
-    (As usual, $m:\hom_A(y,x)$ is a \define{monomorphism} (or is \define{monic}) if $(m\circ f = m\circ g) \Rightarrow (f=g)$.)
+    (As usual, $m:\hom_A(y,x)$ is a \define{monomorphism} (or is \define{monic}) if $(m\circ f = m\circ g) \Rightarrow (f=g)$).
   \item Its morphisms from $(y,m)$ to $(z,n)$ are arbitrary morphisms from $y$ to $z$ in $A$ (not necessarily respecting $m$ and $n$).
   \end{itemize}
   An equality $(y,m)=(z,n)$ of objects in $\mathsf{mono}(A,x)$ consists of an equality $p:y=z$ and an equality $\trans{p}{m}=n$, which by \autoref{ct:idtoiso-trans} is equivalently an equality $m=n\circ \idtoiso(p)$.
@@ -1565,7 +1565,7 @@ \section{The Rezk completion}
   This follows by path induction on $p$ and the third constructor.
 
   The type $\widehat A_0$ will be the type of objects of $\widehat A$; we now build all the rest of the structure.
-  (The following proof is of the sort that can benefit a lot from the help of a computer proof assistant:\index{proof!assistant} it is wide and shallow with many short cases to consider, and a large part of the work consists of writing down what needs to be checked.)
+  (The following proof is of the sort that can benefit a lot from the help of a computer proof assistant:\index{proof!assistant} it is wide and shallow with many short cases to consider, and a large part of the work consists of writing down what needs to be checked).
 
   \mentalpause
 
@@ -1661,7 +1661,7 @@ \section{The Rezk completion}
   That is, for all $x:\widehat A$ we want there to merely exist an $a:A$ such that $Ia\cong x$.
   As always, we argue by induction on $x$, and since the goal is a mere proposition, all but the first constructor are trivial.
   But if $x$ is $ia$, then of course we have $a:A$ and $Ia\jdeq ia$, hence $Ia \cong ia$.
-  (Note that if we were trying to prove $I$ to be \emph{split} essentially surjective, we would be stuck, because we know nothing about equalities in $A_0$ and thus have no way to deal with any further constructors.)
+  (Note that if we were trying to prove $I$ to be \emph{split} essentially surjective, we would be stuck, because we know nothing about equalities in $A_0$ and thus have no way to deal with any further constructors).
 \end{proof}
 
 We call the construction $A\mapsto \widehat A$ the \define{Rezk completion},

equivalences.tex

@@ -497,7 +497,7 @@ \section{On the definition of equivalences}
 We have shown that all three definitions of equivalence satisfy the three desirable properties and are pairwise equivalent:
 \[ \iscontr(f) \eqvsym \ishae(f) \eqvsym \biinv(f). \]
 (There are yet more possible definitions of equivalence, but we will stop with these three.
-See \autoref{ex:brck-qinv} and the exercises in this chapter for some more.)
+See \autoref{ex:brck-qinv} and the exercises in this chapter for some more).
 Thus, we may choose any one of them as ``the'' definition of $\isequiv (f)$.
 For definiteness, we choose to define
 \[ \isequiv(f) \defeq \ishae(f).\]
@@ -519,7 +519,7 @@ \section{Surjections and embeddings}
 or a \define{bijection}.
 \indexdef{bijection}%
 \indexsee{function!bijective}{bijection}%
-(We avoid these words for types that are not sets, since in homotopy theory and higher category theory they often denote a stricter notion of ``sameness'' than homotopy equivalence.)
+(We avoid these words for types that are not sets, since in homotopy theory and higher category theory they often denote a stricter notion of ``sameness'' than homotopy equivalence).
 In set theory, a function is a bijection just when it is both injective and surjective.
 The same is true in type theory, if we formulate these conditions appropriately.
 For clarity, when dealing with types that are not sets, we will speak of \emph{embeddings} instead of injections.
@@ -1036,7 +1036,7 @@ \section{Univalence implies function extensionality}
   Give a characterization of this type analogous to \autoref{lem:qinv-autohtpy}.
 
   Can you give an example showing that this type is not generally a mere proposition?
-  (This will be easier after \autoref{cha:hits}.)
+  (This will be easier after \autoref{cha:hits}).
 \end{ex}
 
 \begin{ex}\label{ex:symmetric-equiv}