Add period at end of formula if the sentence ends

equivalences.tex

@@ -449,9 +449,9 @@ \section{Contractible fibers}
 \end{thm}
 \begin{proof}
 Let $P : \iscontr(f)$. We define an inverse mapping $g : B \to A$ by sending each $y : B$ to the center of contraction of the fiber at $y$:
-\[ g(y) \defeq \proj{1}(\proj{1}(Py)) \]
+\[ g(y) \defeq \proj{1}(\proj{1}(Py)). \]
 We can thus define the homotopy $\epsilon$ by mapping $y$ to the witness that $g(y)$ indeed belongs to the fiber at $y$:
-\[ \epsilon(y) \defeq \proj{2}(\proj{1}(P y)) \]
+\[ \epsilon(y) \defeq \proj{2}(\proj{1}(P y)). \]
 It remains to define $\eta$ and $\tau$. This of course amounts to giving an element of $\rcoh{f}{g}{\epsilon}$. By \cref{lem:coh-hfib}, this is the same as giving for each $x:A$ a path from $(gfx,\epsilon(fx))$ to $(x,\refl{fx})$ in the fiber of $f$ over $fx$. But this is easy: for any $x : A$, the type $\hfib{f}{fx}$
 is contractible by assumption, hence such a path must exist. We can construct it explicitly as
 \[\opp{\big(\proj{2}(P(fx))(gfx,\epsilon(fx))\big)} \ct \big(\proj{2}(P(fx)) (x,\refl{fx})\big). \qedhere \]

formal.tex

@@ -1052,7 +1052,7 @@ \section{Basic metatheory}
 an extension of the untyped $\lambda$-calculus. The $\lambda$-calculus 
 has its own notion of computation, namely the computation rule\index{computation rule!for function types}: 
 \[
-  (\lam{x} t)(u) \defeq t[u/x]
+  (\lam{x} t)(u) \defeq t[u/x].
 \]
 This rule, together with the defining equations for the defined constants form
 \emph{rewriting rules}\index{rewriting rule}\index{rule!rewriting} that determine reduction steps for a rewriting 

hlevels.tex

@@ -197,7 +197,7 @@ \section{Definition of \texorpdfstring{$n$}{n}-types}
  This is \cref{thm:isprop-iscontr}.
 
 For the inductive step we need to show
-\[\prd{X : \type} \isprop (\istype{n}(X)) \to \prd{X : \type} \isprop (\istype{\nplusone}(X)) \]
+\[\prd{X : \type} \isprop (\istype{n}(X)) \to \prd{X : \type} \isprop (\istype{\nplusone}(X)). \]
 To show the conclusion of this implication, we need to show that for any type $X$, the type
 \[\prd{x, x' : X}\istype{n}(x = x')\]
 is a mere proposition. By \cref{thm:isprop-forall} or \cref{thm:hlevel-prod}, it suffices to show that for any $x, x' : X$, the type $\istype{n}(x =_X x')$ is a mere
@@ -208,7 +208,7 @@ \section{Definition of \texorpdfstring{$n$}{n}-types}
 Finally, we show that the type of $n$-types is itself an $\nplusone$-type.
 We define this to be:
 \symlabel{universe-of-ntypes}
-\[\ntype{n} \defeq \sm{X : \type} \istype{n}(X) \]
+\[\ntype{n} \defeq \sm{X : \type} \istype{n}(X). \]
 If necessary, we may specify the universe $\UU$ by writing $\ntypeU{n}$.
 In particular, we have $\prop \defeq \ntype{(-1)}$ and $\set \defeq \ntype{0}$, as defined in \cref{cha:basics}.
 Note that just as for \prop and \set, because $\istype{n}(X)$ is a mere proposition, by \cref{thm:path-subset} for any $(X,p), (X',p'):\ntype{n}$ we have
@@ -805,7 +805,7 @@ \section{Colimits of \texorpdfstring{$n$}{n}-types}
 and a map $t:D\to{}E$, there is a map
   \[\function{\cocone{\Ddiag}{D}}{\cocone{\Ddiag}{E}}{c}{\composecocone{t}c}\]
   defined by:
-  \[\composecocone{t}(i,j,h)=(t\circ{}i,t\circ{}j,\mapfunc{t}\circ{}h)\]
+  \[\composecocone{t}(i,j,h)=(t\circ{}i,t\circ{}j,\mapfunc{t}\circ{}h).\]
 And given $D,E,F$, %$:\P$,
 functions $t:D\to{}E$, $u:E\to{}F$ and $c:\cocone{\Ddiag}{D}$, we have
 \begin{align}
@@ -1327,7 +1327,7 @@ \section{Connectedness}
 truncations, it suffices to give a map $\mathsf{back} : B \to {\trunc{n}{A}}$.  We can
 define this map as follows:
 \[
-\mathsf{back}(y) \defeq \trunc{n}{\proj{1}}{(\proj{1}{(c(y))})}
+\mathsf{back}(y) \defeq \trunc{n}{\proj{1}}{(\proj{1}{(c(y))})}.
 \]
 By definition, $c(y)$ has type $\iscontr(\trunc n {\hfiber{f}y})$, so its
 first component has type $\trunc n{\hfiber{f}y}$, and we can obtain an
@@ -1339,19 +1339,19 @@ \section{Connectedness}
 
 In one direction, we must show that for all $x:A$,
 \[
-\trunc{n}{\proj{1}}{(\proj{1}{(c(f(x)))})} = \tproj{n}{x}
+\trunc{n}{\proj{1}}{(\proj{1}{(c(f(x)))})} = \tproj{n}{x}.
 \]
 But $\tproj{n}{(x, \refl{f(x)})} : \trunc n{\hfiber{f}{f(x)}}$, and
 $c(f(x))$ says that this type is contractible, so
 \[
-\proj{1}{(c(f(x)))} = \tproj{n}{(x, \refl{})}
+\proj{1}{(c(f(x)))} = \tproj{n}{(x, \refl{})}.
 \]
 Applying $\trunc{n}{\proj{1}}$ to both sides of this equation gives the
 result.
 
 In the other direction, we must show that for all $y:B$,
 \[
-\trunc{n}{f}(\trunc{n}{\proj{1}} (\proj{1}{(c(y))})) = \tproj{n}{y}
+\trunc{n}{f}(\trunc{n}{\proj{1}} (\proj{1}{(c(y))})) = \tproj{n}{y}.
 \]
 $\proj{1}{(c(y))}$ has type $\trunc n {\hfiber{f}y}$, and the path we
 want is essentially the second component of the $\hfiber{f}y$, but we

induction.tex

@@ -124,9 +124,10 @@ \section{Introduction to inductive types}
 \end{thm}
 
 \begin{proof}
-We use induction on the type family $D(x) \defeq \id{f(x)}{g(x)}$. For the base case, we have \[f(0) = e_z = g(0)\]
+We use induction on the type family $D(x) \defeq \id{f(x)}{g(x)}$. For the base case, we have
+\[ f(0) = e_z = g(0). \]
 For the inductive case, assume $n : \nat$ such that $f(n) = g(n)$. Then
-\[ f(\suc(n)) = e_s(n, f(n)) = e_s(n, g(n)) = g(\suc(n)) \]
+\[ f(\suc(n)) = e_s(n, f(n)) = e_s(n, g(n)) = g(\suc(n)). \]
 The first and last equality follow from the assumptions on $f$ and $g$. The middle equality follows from the inductive hypothesis and the fact that application preserves equality. This gives us pointwise equality between $f$ and $g$; invoking function extensionality finishes the proof.
 \end{proof}
 
@@ -313,9 +314,10 @@ \section{\texorpdfstring{$\w$}{W}-types}
 
 Clearly, $e$ will be a function taking $a : \bool$ as its first argument. The next step is to perform case analysis on $a$ and proceed based on whether it is $\bfalse$ or $\btrue$. This suggests the following form
 \[ e \defeq \lamu{a:\bool} \rec\bool(C,e_0,e_1,a) \]
-where \[C \defeq \prd{f : B(a) \to \natw}{g : B(a) \to \natw} \natw\]
+where
+\[ C \defeq \prd{f : B(a) \to \natw}{g : B(a) \to \natw} \natw. \]
 If $a$ is $\bfalse$, the type $B(a)$ becomes $\emptyt$. Thus, given $f : \emptyt \to \natw$ and $g : \emptyt \to \natw$, we want to construct an element of $\natw$. Since the label $\bfalse$ represents $\emptyt$, it needs zero inductive arguments and the variables $f$ and $g$ are irrelevant. We return $\zerow$\index{zero} as a result:
-\[ e_0 \defeq \lamu{f:\emptyt \to \natw}{g:\emptyt \to \natw} \zerow \]
+\[ e_0 \defeq \lamu{f:\emptyt \to \natw}{g:\emptyt \to \natw} \zerow. \]
 Analogously, if $a$ is $\btrue$, the type $B(a)$ becomes $\unit$.
 Since the label $\btrue$ represents the successor\index{successor} operator, it needs one inductive argument --- the predecessor\index{predecessor} --- which is represented by the variable $f : \unit \to \natw$.
 The value of the recursive call on the predecessor is represented by the variable $g : \unit \to \natw$.

preliminaries.tex

@@ -504,8 +504,7 @@ \section{Dependent function types (\texorpdfstring{$\Pi$}{Π}-types)}
 For instance, if $a:A$, then writing $\idfunc(a)$ is unambiguous, since $\idfunc$ must mean $\idfunc[A]$ in order for it to be applicable to $a$.
 
 Another, less trivial, example of a polymorphic function is the ``swap'' operation that switches the order of the arguments of a (curried) two-argument function:
-\[ \mathsf{swap} : \prd{A:\UU}{B:\UU}{C:\UU} (A\to B\to C) \to (B\to A \to C)
-\]
+\[ \mathsf{swap} : \prd{A:\UU}{B:\UU}{C:\UU} (A\to B\to C) \to (B\to A \to C). \]
 We can define this by
 \[ \mathsf{swap}(A,B,C,g) \defeq \lam{b}{a} g(a)(b). \]
 We might also equivalently write the type arguments as subscripts:
@@ -519,8 +518,7 @@ \section{Dependent function types (\texorpdfstring{$\Pi$}{Π}-types)}
 arguments.
 (Like $\lambda$-abstractions, $\Pi$s automatically scope\index{scope} over the rest of the expression unless delimited; thus $C : \prd{x:A}B(x) \to \UU$ means $C : \prd{x:A}(B(x) \to \UU)$.)
 In the case when $B$ is constant and equal to $A$, we may condense the notation and write $\prd{x,y:A}$; for instance, the type of $\mathsf{swap}$ could also be written as
-\[ \mathsf{swap} : \prd{A,B,C:\UU} (A\to B\to C) \to (B\to A \to C).
-\]
+\[ \mathsf{swap} : \prd{A,B,C:\UU} (A\to B\to C) \to (B\to A \to C). \]
 Finally, given $f:\prd{x:A}{y : B(x)} C(x,y)$ and arguments $a:A$ and $b:B(a)$, we have $f(a)(b) : C(a,b)$, which,
 as before, we write as $f(a,b) : C(a,b)$.
 
@@ -1374,7 +1372,7 @@ \section{Propositions as types}
 with a ``hole'' $\Box$ of type $A+B\to\emptyt$ indicating what remains to be done.
 (We could equivalently write $f \defeq \rec{(A\to\emptyt)\times (B\to\emptyt)}(A+B\to\emptyt,\lam{x}{y} \Box)$, using the recursor instead of pattern matching.)
 The next phrase ``also suppose $A$ or $B$; we will derive a contradiction'' indicates filling this hole by a function definition, introducing another unnamed hypothesis $z:A+B$, leading to the proof state:
-\[ f((x,y))(z) \defeq \;\Box\; :\emptyt \]
+\[ f((x,y))(z) \defeq \;\Box\; :\emptyt. \]
 Now saying ``there are two cases'' indicates a case split, i.e.\ an application of the recursion principle for the coproduct $A+B$.
 If we write this using the recursor, it would be
 \[ f((x,y))(z) \defeq \rec{A+B}(\emptyt,\lam{a} \Box,\lam{b}\Box,z) \]

setmath.tex

@@ -205,7 +205,7 @@ \subsection{Images}
 Of course when $x$ is $t$ we have $\refl{t}:t=t$, so it suffices to find
 \begin{align*}
 I_0 & : \prd{b:B} \iota(b)= t\\
-I_1 & : \prd{a:A} \opp{\alpha_1(a)} \ct I_0(f(a))=\refl{t}.
+I_1 & : \prd{a:A} \opp{\alpha_1(a)} \ct I_0(f(a))=\refl{t}
 \end{align*}
 where $\iota:B\to C_f$ and $\alpha_1:\prd{a:A} \iota(f(a))= t$ are the other constructors
 of $C_f$. Note that $\alpha_1$ is a homotopy from $\iota\circ f$ to
@@ -362,7 +362,7 @@ \subsection{Quotients}\label{subsec:quotients}
 
 The second construction of quotients is as the set of equivalence classes of $R$ (a subset
 of its power set\index{power set}):
-\[ A\sslash R \defeq \setof{ P:A\to\prop | P \text{ is an equivalence class of } R} \]
+\[ A\sslash R \defeq \setof{ P:A\to\prop | P \text{ is an equivalence class of } R}. \]
 This requires propositional resizing\index{propositional resizing}\index{impredicative!quotient}\index{resizing} in order to remain in the same universe as $A$ and $R$.
 
 Note that if we regard $R$ as a function from $A$ to $A\to \prop$, then $A\sslash R$ is equivalent to $\im(R)$, as constructed in \cref{sec:image}.