From 3277ef1d166cc02db4636228fc91598d7f112b20 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 18:31:07 +0100
Subject: Fix 194--216.

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

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 2930abf..b848db6 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -258,12 +258,14 @@ polymorphism requires a global analysis, replacing the polymorphic bound with a
 
 \subsubsection*{Eliminator Encodings}
 
-This encoding strategy generalises Church encodings. Rather than encoding
-inductive types by their folds, eliminator encodings represent inductive types
-as a product of all their (contravariant) consumers. For example, if we know the
-only operations we will perform on a binary tree are finding the sum of all
-leaves and the depth of the tree. We can encode the binary tree as a pair \(\nat
-\times \nat\), where the first value is the sum and the second is the depth.
+This encoding strategy generalises Church encodings. Rather than
+encoding inductive types by their folds, eliminator encodings
+represent inductive types as a product of some of their
+(contravariant) consumers~\cite{eliminator-enc}. For example, if we
+know the only operations we will perform on a binary tree are finding
+the sum of all leaves and the depth of the tree. We can encode the
+binary tree as a pair \(\nat \times \nat\), where the first value is the
+sum and the second is the depth.
 
 In this encoding, the constructors eagerly compute the results of
 eliminators. With our sum and depth example, we encode the
-- 
cgit v1.2.3

