From de3138bfe231b3bcf052eec12216957b8e7a12ef Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 14:49:17 +0100
Subject: Fix 653--655.

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

(limited to 'sec/encoding.ltx')

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
-- 
cgit v1.2.3

