Fix 283--310.

1 files changed, 20 insertions, 20 deletions

diff --git a/sec/lang.ltx b/sec/lang.ltx
index 1319d5e..e4465fd 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -38,29 +38,29 @@
 In this section we introduce \lang{}, a simply-typed lambda calculus
 with \emph{regular types}.  \Cref{fig:artist-wf} shows the
 well-formedness judgement for types, where \(\jdgmnt{ty}{\Psi}{A}\) means
-that \(A\) is a type using variables from \(\Psi\). Notice that for arrow
-types, the variable context is empty for both premises. Allowing
-variables on the left of arrows leads to non-strictly positive types,
-which in general are impossible to locally encode in
-System~T. Consider for example the positive type \(\mu X. (X \to \nat) \to
-\nat\). In the \(\mathsf{Set}\) model of System~T, this type must be
-represented by an infinite set containing its power set. There is no
-System~T type with this property, thus we should forbid this type. We
-also forbid variables on the right of arrows. For example, consider
-the type \(\mu X. 1 + (\nat \to X)\) of countable trees. None of the
-general encoding strategies work for this type; G\"odel and heap
-encodings both require constructors that perform infinite work, whilst
-Church and codata encodings would be
-global\footnote{\textcite{DBLP:books/sp/LongleyN15} claim the type
-unrepresentable in some models of System~T}.
-
+that \(A\) is a type using variables from \(\Psi\). Types satisfy the
+following substitution lemma:
 \begin{proposition}[Type substitution]
-  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}{\suball{A}{f}}\).
+  For any type \(A\) such that \(\jdgmnt{ty}{\Psi}{A}\) and any type
+  environment \(\alpha\) that assigns each variable \(X \in \Psi\) to a type
+  \(\jdgmnt{ty}{\Theta}{\alpha(X)}\), we have \(\jdgmnt{ty}{\Theta}{\suball{A}{\alpha}}\).
 \end{proposition}
 
+Notice that for arrow types, the variable context is empty for both
+premises. Allowing variables on the left of arrows leads to
+non-strictly positive types, which in general are impossible to
+locally encode in System~T. Consider for example the positive type \(\mu
+X. (X \to \nat) \to \nat\). In the \(\mathsf{Set}\) model of System~T,
+this type must be represented by an infinite set containing its power
+set. The \(\mathsf{Set}\) model has no System~T type with this
+property, thus we should forbid this type. We also forbid variables on
+the right of arrows. For example, consider the type \(\mu X. 1 + (\nat \to
+X)\) of countable trees. None of the general encoding strategies work
+for this type; G\"odel and heap encodings would both require
+constructors that perform infinite work, whilst Church and codata
+encodings would be global\footnote{\textcite{DBLP:books/sp/LongleyN15}
+claim the type unrepresentable in some models of System~T}.
+
 \begin{figure}
   \[
   \begin{array}{cccc}