From 9201b67cc06b411478dec43a56617f7e5b9111d1 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 15:08:49 +0100
Subject: Fix 706--708.

---
 sec/encoding.ltx | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index deddd37..b7029f3 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -465,9 +465,12 @@ it within its type. Secondly, a product can store values from
 different types whilst a list is homogeneous, so we need to use the
 union to make it homogeneous.
 
-We encode tupling \(\tuple{\rangeover{t_i}{i}}\) as the case split \(\lambda
-x. \casetm{x}{i}{\mathsf{inj}~i~t_i}{i}\). The projection \(t.i\) is
-encoded as the application \(\mathsf{prj}~(t~i)~i\).
+To encode products, we must fix an injection \(I \hookrightarrow \mathbb{N}\) for each set of
+labels \(I\). As \(I\) is finite, we can compare a given index against
+the representation \(i_\ell\) of each label \(\ell\). Thus a tuple
+\(\tuple{\rangeover{\ell : t_\ell}{\ell}}\) is encoded as the case split \((\lambda
+x. \casetm{x}{i_\ell}{\mathsf{inj}~\ell~t_\ell}{\ell})\). The projection \(t.\ell\)
+is encoded as the application \(\mathsf{prj}~(t~i_\ell)~\ell\).
 
 At this phase the encodings of our example functions,
 \systemtinline{balanced} and \systemtinline{compose'}, become too
-- 
cgit v1.2.3

