From bd68330d659f1d722f47a843571438389b3d02d5 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 18:28:17 +0100
Subject: Fix 175--182.

---
 sec/systemt.ltx | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'sec/systemt.ltx')

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
   &
-- 
cgit v1.2.3

