From 5e761082beffb918bc754b6631d46a232f7afaab Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 25 Jun 2025 17:01:15 +0100
Subject: Fix figures 4 and 5.

---
 sec/lang.ltx | 43 ++++++++++++++++++++++---------------------
 1 file changed, 22 insertions(+), 21 deletions(-)

(limited to 'sec/lang.ltx')

diff --git a/sec/lang.ltx b/sec/lang.ltx
index 689a9bf..a3d2cb7 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -18,13 +18,13 @@
     \end{prooftree}
     \quad
     \begin{prooftree}
-      \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_i}}{i}}
-      \infer1{\jdgmnt{ty}{\Psi}{\prod_i A_i}}
+      \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_\ell}}{\ell}}
+      \infer1{\jdgmnt{ty}{\Psi}{\prod_{\ell \in I} A_\ell}}
     \end{prooftree}
     \quad
     \begin{prooftree}
-      \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_i}}{i}}
-      \infer1{\jdgmnt{ty}{\Psi}{\sum_i A_i}}
+      \hypo{\rangeover{\jdgmnt{ty}{\Psi}{A_\ell}}{\ell}}
+      \infer1{\jdgmnt{ty}{\Psi}{\sum_{\ell \in I} A_\ell}}
     \end{prooftree}
     \quad
     \begin{prooftree}
@@ -38,8 +38,9 @@
 In this section we introduce \lang{}, a simply-typed lambda calculus
 with \emph{regular types}.  \Cref{fig:artist-wf} shows the
 well-formedness judgement for types, where \(\jdgmnt{ty}{\Psi}{A}\) means
-that \(A\) is a type using variables from \(\Psi\). Types satisfy the
-following substitution lemma:
+that \(A\) is a type using variables from \(\Psi\). We have labelled
+\(n\)-ary products and sums, where the set of labels is finite. Types
+satisfy the following substitution lemma:
 \begin{proposition}[Type substitution]
   For any type \(A\) such that \(\jdgmnt{ty}{\Psi}{A}\) and any type
   environment \(\alpha\) that assigns each variable \(X \in \Psi\) to a type
@@ -63,7 +64,7 @@ claim the type unrepresentable in some models of System~T}.
 
 \begin{figure}
   \[
-  \begin{array}{cccc}
+  \begin{array}{ccc}
     \begin{prooftree}
       \hypo{x : A \in \Gamma}
       \infer1{\judgement{\Gamma}{x}{A}}
@@ -79,40 +80,40 @@ claim the type unrepresentable in some models of System~T}.
       \hypo{\judgement{\Gamma}{t}{A}}
       \infer2{\judgement{\Gamma}{f~t}{B}}
     \end{prooftree}
-    &
+    \\\\
     \begin{prooftree}
       \hypo{\judgement{\Gamma}{t}{A}}
       \hypo{\judgement{\Gamma, x : A}{u}{B}}
       \infer2{\judgement{\Gamma}{\lettm{t}{x}{u}}{B}}
     \end{prooftree}
-    \\\\
+    &
     \begin{prooftree}
-      \hypo{\rangeover{\judgement{\Gamma}{t_i}{A_i}}{i}}
-      \infer1{\judgement{\Gamma}{\tuple{\rangeover{t_i}{i}}}{\prod_i A_i}}
+      \hypo{\rangeover{\judgement{\Gamma}{t_\ell}{A_\ell}}{\ell}}
+      \infer1{\judgement{\Gamma}{\tuple{\rangeover{\ell: t_\ell}{\ell}}}{\prod_{\ell \in I} A_\ell}}
     \end{prooftree}
     &
     \begin{prooftree}
-      \hypo{\judgement{\Gamma}{t}{\prod_i A_i}}
-      \infer1{\judgement{\Gamma}{t.i}{A_i}}
+      \hypo{\judgement{\Gamma}{t}{\prod_{\ell \in I} A_\ell}}
+      \infer1{\judgement{\Gamma}{t.\hat{\ell}}{A_{\hat{\ell}}}}
     \end{prooftree}
-    &
+    \\\\
     \begin{prooftree}
-      \hypo{\judgement{\Gamma}{t}{A_i}}
-      \infer1{\judgement{\Gamma}{\tuple{i, t}}{\sum_i A_i}}
+      \hypo{\judgement{\Gamma}{t}{A_{\hat{\ell}}}}
+      \infer1{\judgement{\Gamma}{\hat{\ell}~t}{\sum_{\ell \in I} A_\ell}}
     \end{prooftree}
     &
+    \multicolumn{2}{c}{
     \begin{prooftree}
-      \hypo{\judgement{\Gamma}{t}{\sum_i A_i}}
-      \hypo{\rangeover{\judgement{\Gamma, x_i : A_i}{t_i}{B}}{i}}
-      \infer2{\judgement{\Gamma}{\casetm{t}{\tuple{i,x_i}}{t_i}{i}}{B}}
+      \hypo{\judgement{\Gamma}{t}{\sum_{\ell \in I} A_\ell}}
+      \hypo{\rangeover{\judgement{\Gamma, x_\ell : A_\ell}{t_\ell}{B}}{\ell}}
+      \infer2{\judgement{\Gamma}{\casetm{t}{\ell~x_\ell}{t_\ell}{\ell}}{B}}
     \end{prooftree}
+    }
     \\\\
-    \multicolumn{2}{c}{
     \begin{prooftree}
       \hypo{\judgement{\Gamma}{t}{\sub{A}{X/\mu X. A}}}
       \infer1{\judgement{\Gamma}{\roll~t}{\mu X. A}}
     \end{prooftree}
-    }
     &
     \multicolumn{2}{c}{
     \begin{prooftree}
-- 
cgit v1.2.3

