Fix 175--182.

1 files changed, 7 insertions, 6 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 1295654..041f89b 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -206,12 +206,13 @@ fold.
 
 \subsubsection*{Church Encodings}
 
-Typically used in untyped settings, Church encodings represent data by their
-fold operation. For example binary trees are Church encoded by the type \(\forall A.
-(\nat \to A) \to (A \to A \to A) \to A\). The first argument describes how to deconstruct
-leaves, and the second applies the inductive step on branches. This encoding
-makes implementing fold trivial. Constructors for the inductive types are also
-simple to encode, as demonstrated by the following example:
+Typically used in untyped settings, Church encodings represent data by
+their fold operation~\cite{church}. For example binary trees are
+Church encoded by the type \(T = \forall A.  (\nat \to A) \to (A \to A \to A) \to
+A\). The first argument describes how to deconstruct leaves, and the
+second applies the inductive step on branches. This encoding makes
+implementing fold trivial. Constructors for the inductive types are
+also simple to encode, as demonstrated by the following example:
 \begin{align*}
   \mathsf{leaf}(n) &\coloneq \lambda l, b.~l~n
   &