Merge pull request #1188 from danielzgtg/fix/unspaceEmDashes

Unify em dashes to spaced version

Author: mikeshulman

.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 em dash style
+        run: "! grep -r '[^ ]---[^ ]' --include='*.tex' || { echo 'Please space 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

@@ -47,7 +47,7 @@ \chapter{Homotopy type theory}
 For example, because
 $p \ct \opp p$ walks out and back along the same route, you know that
 you can continuously shrink $p \ct \opp p$ down to the identity
-path---it won't, for example, get snagged around a hole in the space.
+path --- it won't, for example, get snagged around a hole in the space.
 Homotopy is an equivalence relation, and operations such as
 concatenation, inverses, etc., respect it.  Moreover, the homotopy
 equivalence classes of loops\index{loop} at some point $x_0$ (where two loops $p$
@@ -166,10 +166,10 @@ \chapter{Homotopy type theory}
 description of spaces, in the following sense. Synthetic geometry is geometry in the style of Euclid~\cite{Euclid}: one starts from some basic notions (points and lines), constructions (a line connecting any two points), and axioms
 (all right angles are equal), and deduces consequences logically.  This is in contrast with analytic
 \index{analytic mathematics}%
-geometry, where notions such as points and lines are represented concretely using cartesian coordinates in $\R^n$---lines are sets of points---and the basic constructions and axioms are derived from this representation.  While classical homotopy theory is analytic (spaces and paths are made of points), homotopy type theory is synthetic: points, paths, and paths between paths are basic, indivisible, primitive notions.
+geometry, where notions such as points and lines are represented concretely using cartesian coordinates in $\R^n$ --- lines are sets of points --- and the basic constructions and axioms are derived from this representation.  While classical homotopy theory is analytic (spaces and paths are made of points), homotopy type theory is synthetic: points, paths, and paths between paths are basic, indivisible, primitive notions.
 
-Moreover, one of the amazing things about homotopy type theory is that all of the basic constructions and axioms---all of the
-higher groupoid structure---arises automatically from the induction
+Moreover, one of the amazing things about homotopy type theory is that all of the basic constructions and axioms --- all of the
+higher groupoid structure --- arises automatically from the induction
 principle for identity types.
 Recall from \cref{sec:identity-types} that this says that if
 \begin{itemize}

categories.tex

@@ -1739,7 +1739,7 @@ \section{The Rezk completion}
 When interpreted in Voevodsky's simplicial\index{simplicial!sets} set model of univalent foundations, our precategories are similar to a truncated analogue of Rezk's ``Segal spaces'', while our categories correspond to his ``complete Segal spaces''.
 \index{Segal!category}%
 Strict categories correspond instead to (a weakened and truncated version of) what are called ``Segal categories''.
-It is known that Segal categories and complete Segal spaces are equivalent models for $(\infty,1)$-categories (see e.g.~\cite{bergner:infty-one}), so that in the simplicial set model, categories and strict categories yield ``equivalent'' category theories---although as we have seen, the former still have many advantages.
+It is known that Segal categories and complete Segal spaces are equivalent models for $(\infty,1)$-categories (see e.g.~\cite{bergner:infty-one}), so that in the simplicial set model, categories and strict categories yield ``equivalent'' category theories --- although as we have seen, the former still have many advantages.
 However, in the more general categorical semantics of a higher topos,
 \index{.infinity1-topos@$(\infty,1)$-topos}%
 a strict category corresponds to an internal category (in the traditional sense) in the corresponding 1-topos\index{topos} of sheaves, while a category corresponds to a \emph{stack}.

formal.tex

@@ -31,11 +31,11 @@ \chapter{Formal type theory}
 There are two aspects of type theory which we must pin down before addressing
 such questions. Recall from the Introduction that type theory
 comprises a set of rules specifying when the judgments $a:A$ and $a\jdeq a':A$
-hold---for example, products are characterized by the rule that whenever $a:A$
+hold --- for example, products are characterized by the rule that whenever $a:A$
 and $b:B$, $(a,b):A\times B$. To make this precise, we must first define
-precisely the syntax of terms---the objects $a,a',A,\dots$ which these judgments
+precisely the syntax of terms --- the objects $a,a',A,\dots$ which these judgments
 relate; then, we must define precisely the judgments and their rules of
-inference---the manner in which judgments can be derived from other judgments.
+inference --- the manner in which judgments can be derived from other judgments.
 
 In this appendix, we present two formulations of Martin-L\"{o}f type
 theory, and of the extensions that constitute homotopy type theory.
@@ -1184,7 +1184,7 @@ \section{Basic metatheory}
 
 The consistency\index{consistency} of Martin-L\"{o}f type theory extended with univalence and higher
 inductive types could be shown by inventing an appropriate normalization procedure, but currently
-the only proofs that these systems are consistent are via semantic models---for
+the only proofs that these systems are consistent are via semantic models --- for
 univalence, a model in Kan\index{Kan complex} complexes due to Voevodsky \cite{klv:ssetmodel}, and
 for higher inductive types, a model due to Lumsdaine and Shulman \cite{ls:hits}.
 

hits.tex

@@ -2122,7 +2122,7 @@ \section{The general syntax of higher inductive definitions}
 \index{set-quotient}
 Quotient types are unproblematic in extensional type theory, such as \NuPRL~\cite{constable+86nuprl-book}.
 They are often added by passing to an extended system of setoids.\index{setoid}
-However, quotients are a trickier issue in intensional type theory (the starting point for homotopy type theory), because one cannot simply add new propositional equalities without specifying how they are to behave. Some solutions to this problem have been studied~\cite{hofmann:thesis,Altenkirch1999,altenkirch+07ott}, and several different notions of quotient types have been considered.  The construction of set-quotients using higher-inductives provides an argument for our particular approach (which is similar to some that have previously been considered), because it arises as an instance of a general mechanism.  Our construction does not yet provide a new solution to all the computational problems related to quotients, since we still lack a good computational understanding of higher inductive types in general---but it does mean that ongoing work on the computational interpretation of higher inductives applies to the quotients as well.  The construction of quotients in terms of equivalence classes is, of
+However, quotients are a trickier issue in intensional type theory (the starting point for homotopy type theory), because one cannot simply add new propositional equalities without specifying how they are to behave. Some solutions to this problem have been studied~\cite{hofmann:thesis,Altenkirch1999,altenkirch+07ott}, and several different notions of quotient types have been considered.  The construction of set-quotients using higher-inductives provides an argument for our particular approach (which is similar to some that have previously been considered), because it arises as an instance of a general mechanism.  Our construction does not yet provide a new solution to all the computational problems related to quotients, since we still lack a good computational understanding of higher inductive types in general --- but it does mean that ongoing work on the computational interpretation of higher inductives applies to the quotients as well.  The construction of quotients in terms of equivalence classes is, of
 course, a standard set-theoretic idea, and a well-known aspect of elementary topos theory; its use in type theory (which depends on the univalence axiom, at least for mere propositions) was proposed by Voevodsky.  The fact that quotient types in intensional type theory imply function extensionality was proved by~\cite{hofmann:thesis}, inspired by the work of~\cite{carboni} on exact completions; \cref{thm:interval-funext} is an adaptation of such arguments.
 
 \sectionExercises

hlevels.tex

@@ -1736,8 +1736,8 @@ \section{Modalities}
 
 It may seem odd that every reflective subcategory of types is automatically an exponential ideal, with a product-preserving reflector.
 However, this is also the case classically in the category of \emph{sets}, for the same reasons.
-It's just that this fact is not usually remarked on, since the classical category of sets---in contrast to the category of homotopy
-types---does not have many interesting reflective subcategories.
+It's just that this fact is not usually remarked on, since the classical category of sets --- in contrast to the category of homotopy
+types --- does not have many interesting reflective subcategories.
 
 Two basic properties of $n$-types are \emph{not} shared by general reflective subuniverses: \cref{thm:ntypes-sigma} (closure under $\Sigma$-types) and \cref{thm:truncn-ind} (truncation induction).
 However, the analogues of these two properties are equivalent to each other.

homotopy.tex

@@ -98,7 +98,7 @@ \chapter{Homotopy theory}
 same, where ``the same'' means \emph{homotopy equivalence}
 \index{homotopy!equivalence!topological}%
 (continuous
-maps back and forth that compose to the identity up to homotopy---this
+maps back and forth that compose to the identity up to homotopy --- this
 gives the opportunity to ``correct'' maps that don't exactly compose to
 the identity).  One common way to tell whether two spaces are the same
 is to calculate \emph{algebraic invariants} associated with a space,
@@ -479,7 +479,7 @@ \subsection{The universal cover in type theory}
 Both proofs use the same construction of the cover given above.
 Where the classical proof induces an equivalence on fibers from an equivalence between total spaces, the encode-decode proof constructs the inverse map (\emph{decode}) explicitly as a map between fibers.
 And where the classical proof uses contractibility, the encode-decode proof uses path induction, circle induction, and integer induction.
-These are the same tools used to prove contractibility---indeed, path induction \emph{is} essentially contractibility of the path fibration composed with $\mathsf{transport}$---but they are applied in a different way.
+These are the same tools used to prove contractibility --- indeed, path induction \emph{is} essentially contractibility of the path fibration composed with $\mathsf{transport}$ --- but they are applied in a different way.
 
 Since this is a book about homotopy type theory, we present the encode-decode proof first.
 A homotopy theorist who gets lost is encouraged to skip to the homotopy-theoretic proof (\cref{subsec:pi1s1-homotopy-theory}).
@@ -525,7 +525,7 @@ \subsection{The encode-decode proof}
 \]
 Applying this composition of functions to 0 will compute the
 \index{winding!number}%
-\emph{winding number} of the path---how many times it goes around the
+\emph{winding number} of the path --- how many times it goes around the
 circle, with orientation marked by whether it is positive or negative,
 after inverses have been canceled.  Thus, the computational behavior of
 $\encode$ follows from the reduction rules for higher-inductive types and
@@ -1651,7 +1651,7 @@ \section{The Freudenthal suspension theorem}
 % We have also generalized it to characterize truncations of loop spaces by way of a family of equivalences $\prd{x:A}\code(x) \eqvsym \trunc n{a_0=x}$.
 
 In this case, however, we want to show that $\sigma:X\to \Omega \susp X$ is $2n$-connected.
-We could use a truncated version of the previous method, such as we will see in \cref{sec:van-kampen}, to prove that $\trunc{2n}X\to \trunc{2n}{\Omega \susp X}$ is an equivalence---but this is a slightly weaker statement than the map being $2n$-connected (see \cref{thm:conn-pik,thm:pik-conn}).
+We could use a truncated version of the previous method, such as we will see in \cref{sec:van-kampen}, to prove that $\trunc{2n}X\to \trunc{2n}{\Omega \susp X}$ is an equivalence --- but this is a slightly weaker statement than the map being $2n$-connected (see \cref{thm:conn-pik,thm:pik-conn}).
 However, note that in the general case, to prove that $\decode(x)$ is an equivalence, we could equivalently be proving that its fibers are contractible, and we would still be able to use induction over the base type.
 This we can generalize to prove connectedness of a map into a loop space, i.e.\ that the \emph{truncations} of its fibers are contractible.
 Moreover, instead of constructing $\code$ and $\decode$ separately, we can construct directly a family of \emph{codes for the truncations of the fibers}.

logic.tex

@@ -375,7 +375,7 @@ \section{Classical vs.\ intuitionistic logic}
   % \mathsf{DN}\;\defeq\;
   \prd{A:\UU} \Big(\isprop(A) \to (\neg\neg A \to A)\Big).
 \end{equation}
-The two are also easily seen to be equivalent to each other---see \cref{ex:lem-ldn}---so from now on we will generally speak only of \LEM{}.
+The two are also easily seen to be equivalent to each other --- see \cref{ex:lem-ldn} --- so from now on we will generally speak only of \LEM{}.
 
 This formulation of \LEM{} avoids the ``paradoxes'' of \cref{thm:not-dneg,thm:not-lem}, since \bool is not a mere proposition.
 In order to distinguish it from the more general propositions-as-types formulation, we rename the latter:

preliminaries.tex

@@ -20,7 +20,7 @@ \section{Type theory versus set theory}
 back to Euclid) to use the word ``proposition'' synonymously with ``theorem''.
   We will confine ourselves to the logician's usage, according to which a \emph{proposition} is a statement \emph{susceptible to} proof, whereas a \emph{theorem}\indexfoot{theorem} (or ``lemma''\indexfoot{lemma} or ``corollary''\indexfoot{corollary}) is such a statement that \emph{has been} proven.
 Thus ``$0=1$'' and its negation ``$\neg(0=1)$'' are both propositions, but only the latter is a theorem.}) are identified with particular types, via the correspondence shown in \cref{tab:pov} on page~\pageref{tab:pov}.
-Thus, the mathematical activity of \emph{proving a theorem} is identified with a special case of the mathematical activity of \emph{constructing an object}---in this case, an inhabitant of a type that represents a proposition.
+Thus, the mathematical activity of \emph{proving a theorem} is identified with a special case of the mathematical activity of \emph{constructing an object} --- in this case, an inhabitant of a type that represents a proposition.
 
 \index{deductive system}%
 This leads us to another difference between type theory and set theory, but to explain it we must say a little about deductive systems in general.
@@ -38,7 +38,7 @@ \section{Type theory versus set theory}
 That is, each proposition $A$ gives rise to a judgment ``$A$ has a proof'', and all judgments are of this form.
 A rule of first-order logic such as ``from $A$ and $B$ infer $A\wedge B$'' is actually a rule of ``proof construction'' which says that given the judgments ``$A$ has a proof'' and ``$B$ has a proof'', we may deduce that ``$A\wedge B$ has a proof''.
 Note that the judgment ``$A$ has a proof'' exists at a different level from the \emph{proposition} $A$ itself, which is an internal statement of the theory.
-% In particular, we cannot manipulate it to construct propositions such as ``if $A$ has a proof, then $B$ does not have a proof''---unless we are using our set-theoretic foundation as a meta-theory with which to talk about some other axiomatic system.
+% In particular, we cannot manipulate it to construct propositions such as ``if $A$ has a proof, then $B$ does not have a proof'' --- unless we are using our set-theoretic foundation as a meta-theory with which to talk about some other axiomatic system.
 
 The basic judgment of type theory, analogous to ``$A$ has a proof'', is written ``$a:A$'' and pronounced as ``the term $a$ has type $A$'', or more loosely ``$a$ is an element of $A$'' (or, in homotopy type theory, ``$a$ is a point of $A$'').
 \indexdef{term}%
@@ -82,7 +82,7 @@ \section{Type theory versus set theory}
 Whether or not two expressions are equal by definition is just a matter of expanding out the definitions; in particular, it is algorithmically\index{algorithm} decidable (though the algorithm is necessarily meta-theoretic, not internal to the theory).\index{decidable!definitional equality}
 
 As type theory becomes more complicated, judgmental equality can get more subtle than this, but it is a good intuition to start from.
-Alternatively, if we regard a deductive system as an algebraic theory, then judgmental equality is simply the equality in that theory, analogous to the equality between elements of a group---the only potential for confusion is that there is \emph{also} an object \emph{inside} the deductive system of type theory (namely the type ``$a=b$'') which behaves internally as a notion of ``equality''.
+Alternatively, if we regard a deductive system as an algebraic theory, then judgmental equality is simply the equality in that theory, analogous to the equality between elements of a group --- the only potential for confusion is that there is \emph{also} an object \emph{inside} the deductive system of type theory (namely the type ``$a=b$'') which behaves internally as a notion of ``equality''.
 
 The reason we \emph{want} a judgmental notion of equality is so that it can control the other form of judgment, ``$a:A$''.
 For instance, suppose we have given a proof that $3^2=9$, i.e.\ we have derived the judgment $p:(3^2=9)$ for some $p$.
@@ -577,7 +577,7 @@ \section{Product types}
     an optional \define{uniqueness principle}\indexdef{uniqueness!principle}\footnote{also referred to as \define{$\eta$-expansion}\index{eta-expansion@$\eta $-expansion|footstyle}}, which expresses
 uniqueness of maps into or out of that type.  
 For some types, the uniqueness principle characterizes maps into the type, by stating that 
-every element of the type is uniquely determined by the results of applying eliminators to it, and can be reconstructed from those results by applying a constructor---thus expressing how constructors act on eliminators, dually to the computation rule.  
+every element of the type is uniquely determined by the results of applying eliminators to it, and can be reconstructed from those results by applying a constructor --- thus expressing how constructors act on eliminators, dually to the computation rule.
 (For example, for functions, the uniqueness principle says that any function $f$ is judgmentally equal to the ``expanded'' function $\lamu{x} f(x)$, and thus is uniquely determined by its values.)
 For other types, the uniqueness principle says that every map (function) \emph{from} that type is uniquely determined by some data. (An example is the coproduct type introduced in \cref{sec:coproduct-types}, whose uniqueness principle is mentioned in \cref{sec:universal-properties}.)