diff --git a/paper/gtt.tex b/paper/gtt.tex
index de2b0c9106826730ad3b6afc91cbe99f6d5618d6..9e4a9e4140e4f924d10ab0be9fc8667c98a6d9f3 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -3022,49 +3022,58 @@ type:
\begin{figure}
\begin{mathpar}
\inferrule
- {\Gamma\pipe \Delta \vdash V : \dynv\\
- \Gamma,x_1 : 1\pipe \Delta \vdash E_1 : T\\
- \Gamma,x_\times : \dynv\times\dynv\pipe \Delta \vdash E_\times : T\\
- \Gamma,x_+ : \dynv+\dynv\pipe \Delta \vdash E_+ : T\\
- \Gamma,x_U : U\dync \pipe \Delta \vdash E_U : T\\
- }
- {\Gamma\pipe \Delta \vdash \dyncaseofXthenOnePairSumU {V} {x_{1}. E_1}{x_{\times}. E_{\times}}{x_{+}. E_{+}}{x_{U}. E_U} : T}
-
- \dyncaseofXthenOnePairSumU {(\upcast{G}{\dynv}V)} {x_{1}. E_1}{x_{\times}. E_{\times}}{x_{+}. E_{+}}{x_{U}. E_U} \equidyn E_{G}[V/x_G]\qquad(\dynv\beta)\\
-
- \inferrule
- {\Gamma , x : \dynv \pipe \Delta \vdash E : \u B}
- {E \equidyn \dyncaseofXthenOnePairSumU x
- {x_1. E[\upcast{1}{\dynv}/x_1]}
- {x_{\times}. E[\upcast{{\times}}{\dynv}/x_{\times}]}
- {x_+. E[\upcast{+}{\dynv}/x_+]}
- {x_U. E[\upcast{U}{\dynv}/x_U]}}\quad(\dynv\eta)\\
-
- {\dncast{\u F 1}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_1. \ret x_1}{\els \err}}\\
- {\dncast{\u F(\dynv\times\dynv)}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_\times. \ret x_\times}{\els \err}}\\
- {\dncast{\u F(\dynv + \dynv)}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_+. \ret x_+}{\els \err}}\\
- {\dncast{\u F U\dync}{\u F\dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_U. \ret x_U}{\els \err}}\\
-
- \inferrule
- {\Gamma \pipe \Delta \vdash M_{\to} : \dynv \to \dync\\
- \Gamma \pipe \Delta \vdash M_{\with} : \dync \with \dync\\
- \Gamma \pipe \Delta \vdash M_{\u F} : \u F}
- {\Gamma \pipe \Delta \vdash \dyncocaseWithFunF{M_{\with}}{M_{\to}}{M_{\u F}} : \u B}
-
- \dncast{\u G}{\dync}\dyncocaseWithFunF{M_{\with}}{M_{\to}}{M_{\u F}} \equidyn M_{\u G}\quad(\dync\beta)\\
- {\bullet : \dync \vdash \bullet
- \equidyn
- \dyncocaseWithFunF
- {\dncast{\dync\with\dync}{\dync}\bullet}
- {\dncast{\dynv\to\dync}{\dync}\bullet}
- {\dncast{\u F\dynv}{\dync}\bullet}}\quad(\dync\eta)\\
-
- \force\upcast{U(\dync\with\dync)}{U\dync}V \equidyn \dyncocaseWithFunF{\force V}{\err}{\err}\\
- \force\upcast{U(\dynv \to \dync)}{U\dync}V \equidyn \dyncocaseWithFunF{\err}{\force V}{\err}\\
- \force\upcast{U\u F\dynv}{U\dync}V \equidyn \dyncocaseWithFunF{\err}{\err}{\force V}\\
+ {\Gamma\pipe \Delta \vdash V : \dynv\\
+ \Gamma,x_1 : 1\pipe \Delta \vdash E_1 : T\\
+ \Gamma,x_\times : \dynv\times\dynv\pipe \Delta \vdash E_\times : T\\
+ \Gamma,x_+ : \dynv+\dynv\pipe \Delta \vdash E_+ : T\\
+ \Gamma,x_U : U\dync \pipe \Delta \vdash E_U : T\\
+ }
+ {\Gamma\pipe \Delta \vdash \dyncaseofXthenOnePairSumU {V} {x_{1}. E_1}{x_{\times}. E_{\times}}{x_{+}. E_{+}}{x_{U}. E_U} : T}\and
+
+ \dyncaseofXthenOnePairSumU {(\upcast{G}{\dynv}V)} {x_{1}. E_1}{x_{\times}. E_{\times}}{x_{+}. E_{+}}{x_{U}. E_U} \equidyn E_{G}[V/x_G]\qquad(\dynv\beta)\and
+
+ \inferrule
+ {\Gamma , x : \dynv \pipe \Delta \vdash E : \u B}
+ {E \equidyn \dyncaseofXthenOnePairSumU x
+ {x_1. E[\upcast{1}{\dynv}/x_1]}
+ {x_{\times}. E[\upcast{{\times}}{\dynv}/x_{\times}]}
+ {x_+. E[\upcast{+}{\dynv}/x_+]}
+ {x_U. E[\upcast{U}{\dynv}/x_U]}}\quad(\dynv\eta)\and
+
+ \inferrule
+ {\Gamma \pipe \Delta \vdash M_{\to} : \dynv \to \dync\\
+ \Gamma \pipe \Delta \vdash M_{\with} : \dync \with \dync\\
+ \Gamma \pipe \Delta \vdash M_{\u F} : \u F}
+ {\Gamma \pipe \Delta \vdash \dyncocaseWithFunF{M_{\with}}{M_{\to}}{M_{\u F}} : \u B}\and
+
+ \dncast{\u G}{\dync}\dyncocaseWithFunF{M_{\with}}{M_{\to}}{M_{\u F}} \equidyn M_{\u G}\quad(\dync\beta)\and
+
+ {\bullet : \dync \vdash \bullet
+ \equidyn
+ \dyncocaseWithFunF
+ {\dncast{\dync\with\dync}{\dync}\bullet}
+ {\dncast{\dynv\to\dync}{\dync}\bullet}
+ {\dncast{\u F\dynv}{\dync}\bullet}}\quad(\dync\eta)
\end{mathpar}
\caption{Natural Dynamic Type Extension of GTT}
\end{figure}
+
+The axioms we choose might seem to underspecify the dynamic type, but
+because of the uniqueness of adjoints, the following are derivable.
+\begin{lemma}[Natural Dynamic Type Extension Theorems]
+ The following are derivable in GTT with the natural dynamic type extension
+ \begin{mathpar}
+ {\dncast{\u F 1}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_1. \ret x_1}{\els \err}}\\
+ {\dncast{\u F(\dynv\times\dynv)}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_\times. \ret x_\times}{\els \err}}\\
+ {\dncast{\u F(\dynv + \dynv)}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_+. \ret x_+}{\els \err}}\\
+ {\dncast{\u F U\dync}{\u F\dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_U. \ret x_U}{\els \err}}\\
+ \force\upcast{U(\dync\with\dync)}{U\dync}V \equidyn \dyncocaseWithFunF{\force V}{\err}{\err}\\
+ \force\upcast{U(\dynv \to \dync)}{U\dync}V \equidyn \dyncocaseWithFunF{\err}{\force V}{\err}\\
+ \force\upcast{U\u F\dynv}{U\dync}V \equidyn \dyncocaseWithFunF{\err}{\err}{\force V}\\
+ \end{mathpar}
+\end{lemma}
+We explore this in more detail with the next dynamic type
+interpretation.
\end{longonly}
One of the reasons this dynamic type is so odd is that it includes
@@ -3153,10 +3162,14 @@ This leads to the following definition.
to $\dynv$ by lemma (TODO: ref). Next, we can define $1$ to be the
ep pair to $1+1$ defined by the left case and lemma (TODO: ref).
Then we get the ep pair for $\dynv + \dynv$ by composing the
- isomorphism $\dynv + \dynv \cong (1+1) \times \dynv$ with the ep
- pair for $1+1$:
- \[ \dynv + \dynv \cong (1+1)\times \dynv \triangleleft \dynv \times \dynv \triangleleft \dynv\]
- And similarly for $\dync \with \dync$:
+ isomorphism $(\dynv + \dynv) \cong ((1+1) \times \dynv)$ with the ep
+
+ pair for $1+1$ using the action of product types on ep pairs (proven
+ as part of lemma \ref{lem:casts-are-ep-pairs}):
+ \[ (\dynv + \dynv) \cong ((1+1)\times \dynv) \triangleleft (\dynv \times \dynv) \triangleleft \dynv \]
+ And similarly for $\dync \with \dync$, using the action of the
+ function type on ep pairs (also proven as part of lemma
+ \ref{lem:casts-are-ep-pairs}):
\[ \dync \with \dync \cong (1+1) \to \dync \triangleleft \dynv \to \dync \triangleleft \dync \]
\end{proof}
@@ -3830,6 +3843,7 @@ established we only have to manipulate values and stacks, which
compose much more nicely than effectful terms.
\begin{lemma}[Casts are EP Pairs]
+ \label{lem:casts-are-ep-pairs}
\begin{enumerate}
\item For any $A \ltdyn A'$, the casts $(x.\sem{\upcast{A}{A'}x},
\sem{\dncast{\u F A}{\u F A'}})$ are a value ep pair from