Fix 194--216.

1 files changed, 8 insertions, 6 deletions

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