From 33169dcf49ff1daf69caf4d61f65cbfffd8649fc Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 18:14:59 +0100
Subject: Fix 138--149.

---
 sec/systemt.ltx | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 7ed5870..c9f280b 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -151,19 +151,19 @@ is lacking in some regard.
 
 \subsubsection*{G\"odel Encodings}
 
-G\"odel encodings represent inductive data types as natural
-numbers. It is well-known that there are pairing functions, bijections
-from \(\mathbb{N} \times \mathbb{N}\) to \(\mathbb{N}\), that are primitive recursive. We can use
-these functions to encode inductive types as pairs of tags and
-payloads, such that every constructor has a unique tag. Writing
-\(\tuple{\cdot, \cdot}\) for a chosen pairing function, we can encode the
-binary tree constructors as
+G\"odel encodings~\cite{dialectica?} represent data types as natural
+numbers. It is well-known that there are pairing functions, invertible
+functions from \(\mathbb{N} \times \mathbb{N}\) to \(\mathbb{N}\), that are primitive
+recursive~\cite{pairing}. We can use pairing functions to encode
+inductive types as pairs of tags and payloads, such that every
+constructor has a unique tag. Writing \(\tuple{\cdot, \cdot}\) for a chosen
+pairing function, we can encode the binary tree constructors as
 \begin{align*}
   \mathsf{leaf}(n) &\coloneq \tuple{0, n} \\
   \mathsf{branch}(l, r) &\coloneq \tuple{1, \tuple{l, r}}.
 \end{align*}
-One can pattern match on G\"odel encodings by using the unpairing part of
-the bijection to split a value back into the tag and payload.
+One can pattern match on G\"odel encodings by unpairing a value to
+split it back into the tag and payload.
 
 One major limitation of G\"odel encodings is that they cannot
 represent higher-order data such as functions. The defining trait of
-- 
cgit v1.2.3

