Fix 653--655.

1 files changed, 3 insertions, 3 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 079027a..2d32f30 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -392,9 +392,9 @@ let compose' (depth, heap) =
 
 In this phase we remove sums from the language by encoding them as
 tagged C-style unions, following the work of \textcite{oleg}. We
-encode the type \(\sum_i A_i\) by the pair \(\nat \times \bigsqcup_i A_i\) of
-a tag indicating which case we are in, and a union which can contain a
-value from any case.
+encode the type \(\sum_{\ell \in I} A_\ell\) by the pair \(\nat \times \bigsqcup_{\ell \in I} A_\ell\)
+of a tag indicating the variant, and a union which can contain a value
+from any variant.
 
 Unions have two operators: \(\mathsf{inj}~i~t\) and
 \(\mathsf{prj}~t~i\) for injecting and projecting values at type