Fix 700--706.

1 files changed, 4 insertions, 4 deletions

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