From 934d410d08f22d75418c1affc2e1d3326d2df321 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 15:04:26 +0100
Subject: Fix 700--706.

---
 sec/encoding.ltx | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 45eb639..deddd37 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -457,13 +457,13 @@ let compose (depth, heap) =
 \label{subsec:products}
 
 We will continue following the work of \textcite{oleg} to encode away
-products. A product \(\prod_i A_i\) is encoded as a function \(\nat \to
-\bigsqcup_i A_i\) from indices to values. This is similar to the
+products. A product \(\prod_{\ell \in I} A_\ell\) is encoded as a function \(\nat
+\to \bigsqcup_{\ell \in I} A_\ell\) from labels to values. This is similar to the
 encoding for lists, with only a couple of small variations. First, we
 statically know the length of a product, so we do not need to include
 it within its type. Secondly, a product can store values from
-different types whilst a list is homogenous, so we need to use the
-union to make it homogenous.
+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
-- 
cgit v1.2.3

