Fix 706--708.

1 files changed, 6 insertions, 3 deletions

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