From ad1fc4da5ba668c2fdf0150e59ff5bd2e3ec191e Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 25 Jun 2025 17:18:35 +0100
Subject: Fix map syntax.

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

(limited to 'sec/lang.ltx')

diff --git a/sec/lang.ltx b/sec/lang.ltx
index 02575d8..b26359f 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -161,9 +161,9 @@ our chosen variable \(X \in \Psi\).
     \maptm{X}{X} &\coloneq \lambda f, x. f~x \\
     \maptm{X}{Y} &\coloneq \lambda f, x. x \qquad (X \neq Y)\\
     \maptm{X}{A \to B} &\coloneq \lambda f, x. x \\
-    \maptm{X}{\prod_i A_i} &\coloneq \lambda f, x. \tuple{\rangeover{\maptm{X}{A_i}~f~x.i}{i}} \\
-    \maptm{X}{\sum_i A_i} &\coloneq
-      \lambda f, x. \casetm{x}{\tuple{i,x_i}}{\tuple{i, \maptm{X}{A_i}~f~x_i}}{i} \\
+    \maptm{X}{\prod_{\ell \in I} A_\ell} &\coloneq \lambda f, x. \tuple{\rangeover{\ell : \maptm{X}{A_\ell}~f~x.\ell}{\ell}} \\
+    \maptm{X}{\sum_{\ell \in I} A_\ell} &\coloneq
+      \lambda f, x. \casetm{x}{\ell~x_\ell}{\ell~(\maptm{X}{A_i}~f~x_\ell)}{\ell} \\
     \maptm{X}{\mu Y. A} &\coloneq
     \lambda f, x.
       \dofold{x}{y}{\roll~(\maptm{X}{\sub{A}{Y/\mu Y. \sub{A}{X/C}}}~f~y)}
-- 
cgit v1.2.3

