From 1bd42222da481133db9b8c288039d8c97a289597 Mon Sep 17 00:00:00 2001
From: Jad Ghalayini <jad.ghalayini@protonmail.com>
Date: Mon, 4 Nov 2024 04:19:55 +0000
Subject: [PATCH] Extension runes

---
 paper.tex | 48 ++++++++++++++++++------------------------------
 1 file changed, 18 insertions(+), 30 deletions(-)

diff --git a/paper.tex b/paper.tex
index 877a708..1ae77b9 100644
--- a/paper.tex
+++ b/paper.tex
@@ -3838,6 +3838,22 @@ \subsection{Semantics}
   \item Otherwise, compute $\loopmor{\Gamma}{(\wbranch{\ell_i}{x_i}{t_i},)_i}{\ms{L}}$ in a loop,
   passing in a fresh copy of the context each time. This is implemented with $\ms{rfix}$.
 \end{itemize}
+This simplifies significantly in the case of a \ms{where}-block defining just a single label,
+yielding
+\begin{equation}
+  \dnt{\haslb{\Gamma}{\where{r}{\wbranch{\ell}{x}{s}}}{\ms{L}}}
+  = \lmor{\dnt{\haslb{\Gamma}{r}{\ms{L}, \ell(A)}}}
+  ; \delta^{-1}
+  ; [\pi_r, \rfix{\dnt{\haslb{\Gamma, \bhyp{x}{A}}{s}{\ms{L}, \ell(A)}}}]
+\end{equation}
+In particular, it is a consequence of label weakening (Lemma~\ref{lem:wk}) that, in the case where
+$s$ does not call $\ell$, this simplifies further to
+\begin{equation}
+  \dnt{\haslb{\Gamma}{\where{r}{\wbranch{\ell}{x}{s}}}{\ms{L}}}
+  = \lmor{\dnt{\haslb{\Gamma}{r}{\ms{L}, \ell(A)}}}
+  ; \delta^{-1}
+  ; [\pi_r, \dnt{\haslb{\Gamma, \bhyp{x}{A}}{s}{\ms{L}}}]
+\end{equation}
 
 \begin{figure}
   \begin{equation*}
@@ -3922,6 +3938,7 @@ \subsection{Metatheory}
       $
       \label{itm:lbsubstwk}
   \end{enumerate}
+  \label{lem:wk}
 \end{lemma}
 \begin{proof}
   See Appendix~\ref{proof:weakening}
@@ -5869,13 +5886,6 @@ \section{The Environment Comonad}
   \end{itemize}
 \end{proof}
 
-\TODO{this is useful because of \ms{where}-lore}
-
-\TODO{$\dnt{\haslb{\Gamma, \bhyp{y}{A}}{[\ell/\kappa]s}{\ms{L}}} 
-  = \rfix{S ; [\ms{id}, \iota_r]}$}
-
-\TODO{insert proof of ``$\delta$ lemma?''}
-
 \section{Proofs}
 
 
@@ -6884,28 +6894,6 @@ \subsection{Substitution}
   then follow by a trivial induction.
 \end{proof}
 
-\TODO{immediate consequences of (label) weakening}
-
-\TODO{text}
-
-\begin{equation}
-  \dnt{\haslb{\Gamma}{\where{r}{\wbranch{\ell}{x}{s}}}{\ms{L}}}
-  = \lmor{\dnt{\haslb{\Gamma}{r}{\ms{L}, \ell(A)}}}
-  ; \delta^{-1}
-  ; [\pi_r, \rfix{\dnt{\haslb{\Gamma, \bhyp{x}{A}}{s}{\ms{L}, \ell(A)}}}]
-\end{equation}
-
-\TODO{in particular, if $\haslb{\Gamma, \bhyp{x}{A}}{s}{\ms{L}}$}
-
-\begin{equation}
-  \dnt{\haslb{\Gamma}{\where{r}{\wbranch{\ell}{x}{s}}}{\ms{L}}}
-  = \lmor{\dnt{\haslb{\Gamma}{r}{\ms{L}, \ell(A)}}}
-  ; \delta^{-1}
-  ; [\pi_r, \dnt{\haslb{\Gamma, \bhyp{x}{A}}{s}{\ms{L}}}]
-\end{equation}
-
-\TODO{segue}
-
 \begin{lemma}[Substitution Projection]
   For $\issubst{\gamma}{\Gamma}{\Delta}$, $\ms{eff}(\Delta) = \bot$ and $\Delta(x) = A$, we have
   \begin{equation}
@@ -8173,7 +8161,7 @@ \subsection{Equational Theory}
         = \lmor{R} ; \delta^{-1} ; 
           [\ms{id}, \rfix{S ; [\ms{id}, \iota_r]}] \\
       & = \lmor{R} ; \delta^{-1} ; 
-      [\ms{id}, \rfix{\dnt{\haslb{\Gamma, \bhyp{y}{A}}{[\ell/\kappa]s}{\ms{L}}}}]
+      [\ms{id}, \rfix{\dnt{\haslb{\Gamma, \bhyp{y}{A}}{[\ell/\kappa]s}{\ms{L}, \ell(A)}}}]
         = \dnt{\haslb{\Gamma}{\where{r}{\wbranch{\ell}{y}{[\ell/\kappa]s}}}{\ms{L}}}
       \end{aligned}
     \end{equation}