Fix missing character warning.

4 files changed, 9 insertions, 9 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index cd600ac..3a3cebc 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -174,12 +174,12 @@ prior computations, so we do not need to reference the raw AST.
 \Cref{fig:bidir} shows how we have modified the \lang{} typing rules
 for bidirectional type checking. The changes are
 standard~\cref{bidir}. Products can both check and synthesise types.
-The \rollkw{} operator can only be checked as there is no unique
-correct guess for the shape type. The body of a \foldkw{} must be
-checked. The induction hypothesis is added to the context, so its type
-must be known before processing the body. As the induction hypothesis
-is filled by the motive, the only mode-correct way to obtain the
-motive type is for \foldkw{} to be checked.
+The \roll{} operator can only be checked as there is no unique correct
+guess for the shape type. The body of a \foldkw{} must be checked. The
+induction hypothesis is added to the context, so its type must be
+known before processing the body. As the induction hypothesis is
+filled by the motive, the only mode-correct way to obtain the motive
+type is for \foldkw{} to be checked.
 
 The Idris~2 type for certifying the bidirectional judgement is almost
 a direct translation of the judgement in \cref{fig:bidir}. The
diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index e88a628..0c58aea 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -118,7 +118,7 @@ Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type
 variable \(X \in \Psi\), a type environment \(\alpha\) and a type \(S\), we
 define a term \(\mathsf{distrib}\) of type
 \[
-\submult{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \submult{A}{\alpha}
+\suball{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \suball{A}{\alpha}
 \]
 that calls each accumulator within \(A\) in sequence.  The definition
 is by induction on the well-formedness derivation of \(A\). The
diff --git a/sec/intro.ltx b/sec/intro.ltx
index 0a50ff4..f520bc4 100644
--- a/sec/intro.ltx
+++ b/sec/intro.ltx
@@ -24,7 +24,7 @@
 
 \subsubsection*{Contributions}%
 In this paper we:
-\begin{itemize}
+\begin{itemize}[nosep]
   \item contrast different methods for encoding inductive types in
     System~T (\cref{M-subsec:encoding-strategies});
   \item give the syntax, typing rules and equational theory for
diff --git a/sec/lang.ltx b/sec/lang.ltx
index e675a85..1319d5e 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -58,7 +58,7 @@ unrepresentable in some models of System~T}.
   For any type \(A\) such that \(\jdgmnt{ty}{\Psi}{A}\) and a
   substitution from variables \(X \in \Psi\) to types
   \(\jdgmnt{ty}{\Theta}{f(X)}\), we have
-  \(\jdgmnt{ty}{\Theta}{\submult{A}{f}}\).
+  \(\jdgmnt{ty}{\Theta}{\suball{A}{f}}\).
 \end{proposition}
 
 \begin{figure}