Unify em dashes

Em dashes were annoyingly randomly spaced and unspaced. For consistency,
I chose the unspaced version, based on
https://en.wikipedia.org/wiki/Wikipedia:Manual_of_Style#Dashes .

Author: danielzgtg

.github/workflows/ci.yml

@@ -22,6 +22,9 @@ jobs:
       - name: Fetch all tags for `git describe`
         run: git fetch --force --prune --unshallow --tags
 
+      - name: Check style
+        run: "! grep -r '\( \|^\)--- ' --include='*.tex' || { echo 'Please unspace the em dashes'; exit 1; }"
+
       - name: Update ./errata.tex
         # ./mark-errata should only run on the master branch of the main repo.
         # This job is thus disabled for pull requests and forked repos.

basics.tex

@@ -387,7 +387,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.)
-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.
+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.
 
 \begin{lem}\label{thm:omg}%[The $\omega$-groupoid structure of types]
@@ -405,7 +405,7 @@ \section{Types are higher groupoids}
 
 Note, in particular, that \ref{item:omg1}--\ref{item:omg4} are themselves propositional equalities, living in the identity types \emph{of} identity types, such as $p=_{x=y}q$ for $p,q:x=y$.
 Topologically, they are \emph{paths of paths}, i.e.\ homotopies.
-It is a familiar fact in topology that when we concatenate a path $p$ with the reversed path $\opp p$, we don't literally obtain a constant path (which corresponds to the equality $\refl{}$ in type theory) --- instead we have a homotopy, or higher path, from $p\ct\opp p$ to the constant path.
+It is a familiar fact in topology that when we concatenate a path $p$ with the reversed path $\opp p$, we don't literally obtain a constant path (which corresponds to the equality $\refl{}$ in type theory)---instead we have a homotopy, or higher path, from $p\ct\opp p$ to the constant path.
 
 \begin{proof}[Proof of~\cref{thm:omg}]
   All the proofs use the induction principle for equalities.
@@ -1415,7 +1415,7 @@ \section{\texorpdfstring{$\Sigma$}{Σ}-types}
 Thus, we are saying that a path $w=w'$ in the total space determines (and is determined by) a path $p:\proj1(w)=\proj1(w')$ in $A$ together with a path from $\proj2(w)$ to $\proj2(w')$ lying over $p$, which seems sensible.
 
 \begin{rmk}\label{rmk:sigma-equality-extraction}
-  Note that if we have $x:A$ and $u,v:P(x)$ such that $(x,u)=(x,v)$, it does not follow that $u=v$ --- see \cref{ex:sigma-eq-components-neq} for a counterexample.
+  Note that if we have $x:A$ and $u,v:P(x)$ such that $(x,u)=(x,v)$, it does not follow that $u=v$---see \cref{ex:sigma-eq-components-neq} for a counterexample.
   All we can conclude is that there exists $p:x=x$ such that $\trans p u = v$.
   This is a well-known source of confusion for newcomers to type theory, but it makes sense from a topological viewpoint: the existence of a path $(x,u)=(x,v)$ in the total space of a fibration between two points that happen to lie in the same fiber does not imply the existence of a path $u=v$ lying entirely \emph{within} that fiber.
 \end{rmk}

blurb.tex

@@ -17,10 +17,10 @@
 On the other hand, we have \emph{higher inductive types}, which provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory: spheres, cylinders, truncations, localizations, etc.
 Both ideas are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of ``logic of homotopy types''.
 
-This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an ``invariant'' conception of the objects of mathematics --- and convenient machine implementations, which can serve as a practical aid to the working mathematician.
+This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an ``invariant'' conception of the objects of mathematics---and convenient machine implementations, which can serve as a practical aid to the working mathematician.
 This is the \emph{Univalent Foundations} program.
 
-The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning --- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
+The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning---but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
 We believe that univalent foundations will eventually become a viable alternative to set theory as the ``implicit foundation'' for the unformalized mathematics done by most mathematicians.
 
 \bigskip

equivalences.tex

@@ -206,7 +206,7 @@ \section{Half adjoint equivalences}
 \end{proof}
 
 However, it is important that we do not include \emph{both} $\tau$ and $\upsilon$ in the definition of $\ishae (f)$ (whence the name ``\emph{half} adjoint equivalence'').
-If we did, then after canceling contractible types we would still have one remaining datum --- unless we added another higher coherence condition.
+If we did, then after canceling contractible types we would still have one remaining datum---unless we added another higher coherence condition.
 In general, we expect to get a well-behaved type if we cut off after an odd number of coherences.
 
 Of course, it is obvious that $\ishae(f) \to\qinv(f)$: simply forget the coherence datum.

hits.tex

@@ -107,7 +107,7 @@ \section{Induction principles and dependent paths}
 
 When we describe a higher inductive type such as the circle as being generated by certain constructors, we have to explain what this means by giving rules analogous to those for the basic type constructors from \cref{cha:typetheory}.
 The constructors themselves give the \emph{introduction} rules, but it requires a bit more thought to explain the \emph{elimination} rules, i.e.\ the induction and recursion principles.
-In this book we do not attempt to give a general formulation of what constitutes a ``higher inductive definition'' and how to extract the elimination rule from such a definition --- indeed, this is a subtle question and the subject of current research.
+In this book we do not attempt to give a general formulation of what constitutes a ``higher inductive definition'' and how to extract the elimination rule from such a definition---indeed, this is a subtle question and the subject of current research.
 Instead we will rely on some general informal discussion and numerous examples.
 
 \index{type!circle}%
@@ -1031,8 +1031,8 @@ \section{Pushouts}
 
 \begin{rmk}
   As remarked in \cref{subsec:prop-trunc}, the notations $\wedge$ and $\vee$ for the smash product and wedge of pointed spaces are also used in logic for ``and'' and ``or'', respectively.
-  Since types in homotopy type theory can behave either like spaces or like propositions, there is technically a potential for conflict --- but since they rarely do both at once, context generally disambiguates.
-  Furthermore, the smash product and wedge only apply to \emph{pointed} spaces, while the only pointed mere proposition is $\top\jdeq\unit$ --- and we have $\unit\wedge \unit = \unit$ and $\unit\vee\unit=\unit$ for either meaning of $\wedge$ and $\vee$.
+  Since types in homotopy type theory can behave either like spaces or like propositions, there is technically a potential for conflict---but since they rarely do both at once, context generally disambiguates.
+  Furthermore, the smash product and wedge only apply to \emph{pointed} spaces, while the only pointed mere proposition is $\top\jdeq\unit$---and we have $\unit\wedge \unit = \unit$ and $\unit\vee\unit=\unit$ for either meaning of $\wedge$ and $\vee$.
 \end{rmk}
 
 \index{pushout|)}%
@@ -1073,7 +1073,7 @@ \section{Truncations}
 \item for any $x,y:\brck A$, the function $\apfunc f$ takes the specified path $x=y$ in $\brck A$ to the specified path $f(x) = f(y)$ in $B$ (propositionally).
 \end{itemize}
 \index{recursion principle!for truncation}%
-These are exactly the hypotheses that we stated in \cref{subsec:prop-trunc} for the recursion principle of propositional truncation --- a function $A\to B$ such that $B$ is a mere proposition --- and the first part of the conclusion is exactly what we stated there as well.
+These are exactly the hypotheses that we stated in \cref{subsec:prop-trunc} for the recursion principle of propositional truncation---a function $A\to B$ such that $B$ is a mere proposition---and the first part of the conclusion is exactly what we stated there as well.
 The second part (the action of $\apfunc f$) was not mentioned previously, but it turns out to be vacuous in this case, because $B$ is a mere proposition, so \emph{any} two paths in it are automatically equal.
 
 \index{induction principle!for truncation}%
@@ -1155,7 +1155,7 @@ \section{Truncations}
 Alternatively, we could modify the definition of the pushout in \cref{sec:colimits} to include the $0$-truncation constructor directly, avoiding the need to truncate afterwards.
 Similar remarks apply to any sort of colimit of sets; we will explore this further in \cref{cha:set-math}.
 
-However, while the above definition of the 0-truncation works --- it gives what we want, and is consistent --- it has a couple of issues.
+However, while the above definition of the 0-truncation works---it gives what we want, and is consistent---it has a couple of issues.
 Firstly, it doesn't fit so nicely into the general theory of higher inductive types.
 In general, it is tricky to deal directly with constructors such as the second one we have given for $\trunc0A$, whose \emph{inputs} involve not only elements of the type being defined, but paths in it.
 
@@ -1583,7 +1583,7 @@ \section{Algebra}
 \index{monoid!free|)}%
 
 This construction of the free monoid is possible essentially because elements of the free monoid have computable canonical forms (namely, finite lists).
-However, elements of other free (and presented) algebraic structures --- such as groups --- do not in general have \emph{computable} canonical forms.
+However, elements of other free (and presented) algebraic structures---such as groups---do not in general have \emph{computable} canonical forms.
 For instance, equality of words in group presentations is algorithmically\index{algorithm} undecidable.
 However, we can still describe free algebraic objects as \emph{higher} inductive types, by simply asserting all the axiomatic equations as path constructors.
 
@@ -2062,7 +2062,7 @@ \section{The general syntax of higher inductive definitions}
 
 Note that this order is not necessarily the order of ``dimension'': in principle, a 1-dimensional path constructor could refer to a 2-dimensional one and hence need to come after it.
 However, we have not given the 0-dimensional constructors (point constructors) any way to refer to previous constructors, so they might as well all come first.
-And if we use the hub-and-spoke construction (\cref{sec:hubs-spokes}) to reduce all constructors to points and 1-paths, then we might assume that all point constructors come first, followed by all 1-path constructors --- but the order among the 1-path constructors continues to matter.
+And if we use the hub-and-spoke construction (\cref{sec:hubs-spokes}) to reduce all constructors to points and 1-paths, then we might assume that all point constructors come first, followed by all 1-path constructors---but the order among the 1-path constructors continues to matter.
 
 The remaining question is, what sort of expressions can $u$ and $v$ be?
 We might hope that they could be any expression at all involving the previous constructors.
@@ -2096,7 +2096,7 @@ \section{The general syntax of higher inductive definitions}
 The intuition of naturality supplies only a rough guide for when a higher inductive definition is permissible.
 Even if it were possible to give a precise specification of permissible forms of such definitions in this book, such a specification would probably be out of date quickly, as new extensions to the theory are constantly being explored.
 For instance, the presentation of $n$-spheres in terms of ``dependent $n$-loops\index{loop!dependent n-@dependent $n$-}'' referred to in \cref{sec:circle}, and the ``higher inductive-recursive definitions'' used in \cref{cha:real-numbers}, were innovations introduced while this book was being written.
-We encourage the reader to experiment --- with caution.
+We encourage the reader to experiment---with caution.
 
 
 \sectionNotes
@@ -2107,7 +2107,7 @@ \section{The general syntax of higher inductive definitions}
 
 A general discussion of the syntax of higher inductive types, and their semantics in higher-categorical models, appears in~\cite{ls:hits}.
 As with ordinary inductive types, models of higher inductive types can be constructed by transfinite iterative processes; a slogan is that ordinary inductive types describe \emph{free} monads while higher inductive types describe \emph{presentations} of monads.\index{monad}
-The introduction of path constructors also involves the model-category-theoretic equivalence between ``right homotopies'' (defined using path spaces) and ``left homotopies'' (defined using cylinders) --- the fact that this equivalence is generally only up to homotopy provides a semantic reason to prefer propositional computation rules for path constructors.
+The introduction of path constructors also involves the model-category-theoretic equivalence between ``right homotopies'' (defined using path spaces) and ``left homotopies'' (defined using cylinders)---the fact that this equivalence is generally only up to homotopy provides a semantic reason to prefer propositional computation rules for path constructors.
 
 Another (temporary) reason for this preference comes from the limitations of existing computer implementations.
 Proof assistants\index{proof!assistant} like \Coq and \Agda have ordinary inductive types built in, but not yet higher inductive types.

hlevels.tex

@@ -228,7 +228,7 @@ \section{Definition of \texorpdfstring{$n$}{n}-types}
   is an embedding, so that if $n\geq -1$, then by \cref{thm:isntype-mono} it suffices to show that $X \rightarrow X'$ is an $n$-type.
   But since $n$-types are preserved under the arrow type, this reduces to an assumption that $X'$ is an $n$-type.
 
-  In the case $n=-2$, this argument shows that $\eqv{X}{X'}$ is a $(-1)$-type --- but it is also inhabited, since any two contractible types
+  In the case $n=-2$, this argument shows that $\eqv{X}{X'}$ is a $(-1)$-type---but it is also inhabited, since any two contractible types
 are equivalent to \unit, and hence to each other.
   Thus, $\eqv{X}{X'}$ is also a $(-2)$-type.
 \end{proof}