From 5c056c65391d7066f42ae8ec28d928f91df694e6 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 30 Jan 2020 16:32:15 -0500
Subject: [PATCH] checkin

---
 jfp-paper/defs.tex    |  19 +++
 jfp-paper/jfp-gtt.tex | 276 ++++++++++++++++++++++--------------------
 2 files changed, 167 insertions(+), 128 deletions(-)

diff --git a/jfp-paper/defs.tex b/jfp-paper/defs.tex
index 781407c..21ab426 100644
--- a/jfp-paper/defs.tex
+++ b/jfp-paper/defs.tex
@@ -165,6 +165,25 @@
 \newcommand\cbvtocbpvty[1]{#1^{ty}}
 \newcommand\purely{\downarrow}
 
+% Stack formatting
+\newenvironment{stackAux}[2]{%
+\setlength{\arraycolsep}{0pt}
+\begin{array}[#1]{#2}}{
+\end{array}\ignorespacesafterend}
+\newenvironment{stackCC}{
+\begin{stackAux}{c}{c}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackCL}{
+\begin{stackAux}{c}{l}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackTL}{
+\begin{stackAux}{t}{l}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackTR}{
+\begin{stackAux}{t}{r}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackBC}{
+\begin{stackAux}{b}{c}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackBL}{
+\begin{stackAux}{b}{l}}{\end{stackAux}\ignorespacesafterend}
+
 %% Local Variables:
 %% compile-command: "./latexrun jfp-gtt.tex"
 %% End:
+
diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index 1c8fd81..44b3def 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -1094,29 +1094,31 @@ function position.  The elimination form for $U \u B$, $\force{V}$, is
 the prototypical non-stack computation ($\Delta$ is required to be
 empty), because forcing a thunk does not use the stack's input.
 
-\paragraph{Embedding call-by-value and call-by-name.}  To translate
-call-by-value (CBV) into CBPV, a judgement $x_1 : A_1, \ldots, x_n : A_n
-\vdash e : A$ is interpreted as a computation $x_1 : A_1^v, \ldots, x_n
-: A_n^v \vdash e^v : \u F A^v$, where call-by-value products and sums
-are interpreted as $\times$ and $+$, and the call-by-value function type
-$A \to A'$ as $U(A^v \to \u F A'^v)$.  Thus, a call-by-value term $e : A
-\to A'$, which should mean an effectful computation of a function value,
-is translated to a computation $e^v : \u F U (A^v \to \u F A'^v)$. Here,
-the comonad $\u F U$ offers an opportunity to perform effects
-\emph{before} returning a function value---so under translation the CBV
-terms $\print c; \lambda x. e$ and $\lambda x.\print c; e$ will not be
-contextually equivalent.  To translate call-by-name (CBN) to CBPV, a
-judgement $x_1 : \u B_1, \ldots, x_m : \u B_m \vdash e : \u B$ is
-translated to $x_1 : U \u {B_1}^n, \ldots, x_m : U \u {B_m}^n \vdash e^n
-: \u B^n$, representing the fact that call-by-name terms are passed
-thunked arguments.  Product types are translated to $\top$ and $\times$,
-while a CBN function $B \to B'$ is translated to $U \u B^n \to \u B'^n$
-with a thunked argument.  Sums $B_1 + B_2$ are translated to $\u F (U \u
-{B_1}^n + U \u {B_2}^n)$, making the ``lifting'' in lazy sums explicit.
-Call-by-push-value \emph{subsumes} call-by-value and call-by-name in
-that these embeddings are \emph{full and faithful}: two CBV or CBN programs are
-equivalent if and only if their embeddings into CBPV are equivalent, and
-every CBPV program with a CBV or CBN type can be back-translated.
+\paragraph{Embedding Call-by-value and Call-by-name}  To translate
+from call-by-value (CBV) to CBPV, a CBV expression $x_1 : A_1, \ldots,
+x_n : A_n \vdash e : A$ is interpreted as a computation $x_1 : A_1^v,
+\ldots, x_n : A_n^v \vdash e^v : \u F A^v$, where call-by-value
+products and sums are interpreted as $\times$ and $+$, and the
+call-by-value function type $A \to A'$ as $U(A^v \to \u F A'^v)$.
+Thus, a call-by-value term $e : A \to A'$, which should mean an
+effectful computation of a function value, is translated to a
+computation $e^v : \u F U (A^v \to \u F A'^v)$. Here, the comonad $\u
+F U$ offers an opportunity to perform effects \emph{before} returning
+a function value---so under translation the CBV terms $\print c;
+\lambda x. e$ and $\lambda x.\print c; e$ will not be contextually
+equivalent.  To translate call-by-name (CBN) to CBPV, a judgement $x_1
+: \u B_1, \ldots, x_m : \u B_m \vdash e : \u B$ is translated to $x_1
+: U \u {B_1}^n, \ldots, x_m : U \u {B_m}^n \vdash e^n : \u B^n$,
+representing the fact that call-by-name terms are passed thunked
+arguments.  Product types are translated to $\top$ and $\times$, while
+a CBN function $B \to B'$ is translated to $U \u B^n \to \u B'^n$ with
+a thunked argument.  Sums $B_1 + B_2$ are translated to $\u F (U \u
+{B_1}^n + U \u {B_2}^n)$, making the ``lifting'' in lazy sums
+explicit.  Call-by-push-value \emph{subsumes} call-by-value and
+call-by-name in that these embeddings are \emph{full and faithful}:
+two CBV or CBN programs are equivalent if and only if their embeddings
+into CBPV are equivalent, and every CBPV program with a CBV or CBN
+type can be back-translated.
 
 %% While these rules are very intuitive when the input and output types
 %% of the stack are $\u F A$ for some value type (which is always the
@@ -2037,14 +2039,15 @@ casts:
   \end{mathpar}
 \end{small}
 \end{lemma}
-  In sequent calculus terminology, an upcast is left-invertible, while a
-downcast is right-invertible, in the sense that any time we have a
-conclusion with a upcast on the left/downcast on the right, we can
-without loss of generality apply these rules (this comes from upcasts
-and downcasts forming a Galois connection).  We write the $A \ltdyn A'$
-and $\u B' \ltdyn \u B''$ premises on the non-invertible rules to
-emphasize that the premise is not necessarily well-formed given that the
-conclusion is.
+
+In sequent calculus terminology, in the term dynamism judgement an
+upcast is left-invertible, while a downcast is right-invertible, in
+the sense that any time we have a conclusion with a upcast on the
+left/downcast on the right, we can without loss of generality apply
+these rules (this comes from upcasts and downcasts forming a Galois
+connection).  We write the $A \ltdyn A'$ and $\u B' \ltdyn \u B''$
+premises on the non-invertible rules to emphasize that the premise is
+not necessarily well-formed given that the conclusion is.
 
 \begin{longproof}
 For upcast left, substitute $V'$ into the axiom $x \ltdyn
@@ -2225,22 +2228,27 @@ out of the dynamic type are coherent, for example if $A \ltdyn A'$
 then
 $\upcast{A}{\dynv}{x} \equidyn \upcast{A'}{\dynv}{\upcast{A}{A'}{x}}$.  
 
- The following theorem says essentially that $x \ltdyn
- \dncast{T}{T'}{\upcast{T}{T'}{x}}$ (upcast then downcast might error
- less but but otherwise does not change the behavior) and
- $\upcast{T}{T'}{\dncast{T}{T'}{x}} \ltdyn x$ (downcast then upcast
- might error more but otherwise does not change the behavior).  However,
- since a value type dynamism $A \ltdyn A'$ induces a value upcast $x :
- A \vdash \upcast{A}{A'}{x} : A'$ but a stack downcast $\bullet : \u F
- A' \vdash \dncast{\u F A}{\u F A'}{\bullet} : \u F A$ (and dually for
- computations), the statement of the theorem wraps one cast with 
- the constructors for $U$ and $\u F$ types (functoriality of $\u F/U$).
-\begin{theorem}[Casts are a Galois Connection] \label{thm:cast-adjunction} ~~~
+TODO: rewrite this section using defined casts.
+ %% The following theorem says essentially that $x \ltdyn
+ %% \dncast{T}{T'}{\upcast{T}{T'}{x}}$ (upcast then downcast might error
+ %% less but but otherwise does not change the behavior) and
+ %% $\upcast{T}{T'}{\dncast{T}{T'}{x}} \ltdyn x$ (downcast then upcast
+ %% might error more but otherwise does not change the behavior).  However,
+ %% since a value type dynamism $A \ltdyn A'$ induces a value upcast $x :
+ %% A \vdash \upcast{A}{A'}{x} : A'$ but a stack downcast $\bullet : \u F
+ %% A' \vdash \dncast{\u F A}{\u F A'}{\bullet} : \u F A$ (and dually for
+ %% computations), the statement of the theorem wraps one cast with 
+ %% the constructors for $U$ and $\u F$ types (functoriality of $\u F/U$).
+\begin{theorem}[Casts form Galois Connections] \label{thm:cast-adjunction}
+  If $A \ltdyn A'$, then the following hold
+  \begin{enumerate}
+  \item $\bullet' : \u F A' \vdash \defupcast{\u F A}{\u F A'}\dncast{\u F A}{\u F A'}\bullet' \ltdyn \bullet' : \u F A'$
+  \item $\bullet : \u F A \vdash \bullet \ltdyn \dncast{\u F A}{\u F A'}\defupcast{\u F A}{\u F A'}\bullet : \u F A$
+  \end{enumerate}
+  If $\u B \ltdyn \u B'$, then the following hold
   \begin{enumerate}
-  \item $\bullet' : \u F A' \vdash \bindXtoYinZ{\dncast{\u F A}{\u F A'}{\bullet'}}{x}{\ret{(\upcast{A}{A'}{x})}} \ltdyn \bullet' : \u F A'$
-  \item $\bullet : \u F A \vdash \bullet \ltdyn \bindXtoYinZ{\bullet}{x}{\dncast{\u F A}{\u F A'}{(\ret{(\upcast{A}{A'}{x})})}}  : \u F A$
-  \item $x : U \u B' \vdash {\upcast{U \u B}{U \u B'}{(\thunk{({\dncast{\u B}{\u B'}{\force x}})})}} \ltdyn x : U \u B'$
-  \item $x : U \u B \vdash x \ltdyn \thunk{(\dncast{B}{B'}{(\force{(\upcast{U \u B}{U \u B'}{x})})})} : U \u B$
+  \item $x : U \u B' \vdash {\upcast{U \u B}{U \u B'}\defdncast{U \u B}{U \u B'}x} \ltdyn x : U \u B'$
+  \item $x : U \u B \vdash x \ltdyn \defdncast{U \u B}{U \u B'}\upcast{U \u B}{U \u B'}{x} : U \u B$
   \end{enumerate}
 \end{theorem}
 \begin{longproof} ~
@@ -2323,11 +2331,12 @@ the retraction property for general casts:
 %% \equidyn \dncast{T}{\dynv}{\upcast{T}{\dynv}{x}} \equidyn x
 %% \]
 \begin{theorem}[Retract Property for General Casts] ~~~ \label{thm:retract-general}
+  If $A \ltdyn A'$ and $\u B \ltdyn \u B'$, then
   \begin{enumerate}
   \item
-    $\bullet : \u F A \vdash \bindXtoYinZ{\bullet}{x}{\dncast{\u F A}{\u F A'}{(\ret{(\upcast{A}{A'}{x})})}} \equidyn \bullet  : \u F A$
+    $\bullet : \u F A \vdash \defupcast{\u F A}{\u F A'}\dncast{\u F A}{\u F A'}\bullet \equidyn \bullet  : \u F A$
   \item
-    $x : U \u B \vdash \thunk{(\dncast{\u B}{\u B'}{(\force{(\upcast{U \u B}{U \u B'}{x})})})} \equidyn x : U \u B$
+    $x : U \u B \vdash \defdncast{U\u B}{U\u B'}\upcast{U \u B}{U \u B'}{x} \equidyn x : U \u B$
   \end{enumerate}
 \end{theorem}
 \begin{longproof}
@@ -2596,63 +2605,78 @@ Dually, we have
 Together, the universal property for casts and the $\eta$ principles for
 each type imply that the casts must behave as in lazy cast semantics:
 \begin{theorem}[Cast Unique Implementation Theorem for $+,\times,\to,\with$] \label{thm:functorial-casts}
-The casts' behavior is uniquely determined as follows: \ifshort (See the extended version for $+$, $\with$.) \fi
-\begin{small}
-\[
-   \begin{array}{c}
-\iflong  
-    \upcast{A_1 + A_2}{A_1' + A_2'}{s} \equidyn \caseofXthenYelseZ{s}{x_1.\inl{(\upcast{A_1}{A_1'}{x_1})}}{x_2.\inr{(\upcast{A_2}{A_2'}{x_2})}}\\\\
-    \begin{array}{rcl}
-    \dncast{\u F (A_1' + A_2')}{\u F (A_1 + A_2)}{\bullet} & \equidyn 
-    & \bindXtoYinZ{\bullet}{(s : (A_1' + A_2'))}\caseofX{s}\\
-    & &  \{{x_1'.\bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1'}{(\ret{x_1'})})}{x_1}{\ret{(\inl {x_1})}}} \\
-    & &  \mid {x_2'.\bindXtoYinZ{(\dncast{\u F A_2}{\u F A_2'}{(\ret{x_2'})})}{x_2}{\ret{(\inr {x_2})}}} \}\\
-    \end{array}
-    \\\\
-\fi
-    \upcast{A_1 \times A_2}{A_1' \times A_2'}{p} \equidyn \pmpairWtoXYinZ{p}{x_1}{x_2}{(\upcast{A_1}{A_1'}{x_1},\upcast{A_2}{A_2'}{x_2})} \\\\
-    \begin{array}{rcl}
-    \dncast{\u F (A_1' \times A_2')}{\u F (A_1 \times A_2)}{\bullet} &
-      \equidyn & 
-      \bindXtoYinZ{\bullet}{p'} {\pmpairWtoXYinZ{p'}{x_1'}{x_2'}{}}\\
-      & & \bindXtoYinZ{\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}{x_1}\\
-      & & \bindXtoYinZ{\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}{x_2} {\ret (x_1,x_2) }\\
-\iflong
-      & \equidyn &  
-      \bindXtoYinZ{\bullet}{p'} \pmpairWtoXYinZ{p'}{x_1'}{x_2'}{} \\
-      & & \bindXtoYinZ{\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}{x_2} \\
-      & & \bindXtoYinZ{\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}{x_1} {\ret (x_1,x_2) }
-\fi
-    \end{array}\\\\
-%% if losing space due to not pagebreaking in the middle of this
-%%     \\\\
-%%   \end{array}
-%% \]
-%% \[
-%%   \begin{array}{c}
-\iflong  
-    \dncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}{\bullet} \equidyn 
-    \pair{\dncast{\u B_1}{\u B_1'}{\pi \bullet}}{\dncast{\u B_2}{\u B_2'}{\pi' \bullet}}\\\\
-    \begin{array}{rcll}
-      \upcast{U (\u B_1 \with \u B_2)}{U (\u B_1' \with \u B_2')}{p} & \equidyn &
-      \thunk{} & {\{\pi \mapsto {\force{(\upcast{U \u B_1}{U \u B_1'}{(\thunk{\pi (\force{p})})})}}}\\
-      &&& \pi' \mapsto {\force{(\upcast{U \u B_2}{U \u B_2'}{(\thunk{\pi' (\force{p})})})}} \}
-    \end{array}\\\\
-\fi
-    
-    \dncast{A \to \u B}{A' \to \u B'}{\bullet} \equidyn
-    \lambda{x}.{\dncast{\u B}{\u B'}{(\bullet \, (\upcast{A}{A'}{x}))}} \\\\
+  All of the equivalences in Figure~\ref{fig:uniq-impl} are derivable.
 
-    \begin{array}{rcll}
-      \upcast{U (A \to \u B)}{U (A' \to \u B')}{f} & \equidyn &
-      \thunk (\lambda x'. & \bindXtoYinZ{\dncast{\u F A}{\u F A'}{(\ret x')}}{x}{} \\
-      & & & { \force{(\upcast{U \u B}{U \u B'}{(\thunk{(\force{(f)}\,x)})})}} )
-    \end{array}
-        \\
-  \end{array}
-  \]
-  \end{small}
+  \begin{figure}
+    \begin{footnotesize}
+      \[
+      \begin{array}{c}
+
+        \upcast{A_1 + A_2}{A_1' + A_2'}{s} \equidyn \caseofXthenYelseZ{s}{x_1.\inl{(\upcast{A_1}{A_1'}{x_1})}}{x_2.\inr{(\upcast{A_2}{A_2'}{x_2})}}\\\\
+        \begin{array}{rcl}
+          \dncast{\u F (A_1' + A_2')}{\u F (A_1 + A_2)}{\bullet} & \equidyn 
+          & \bindXtoYinZ{\bullet}{(s : (A_1' + A_2'))}\caseofX{s}\\
+          & &  \{x_1'.
+            \begin{stackTL}
+            \bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1'}{(\ret{x_1'})})}{x_1}\\ {\ret{(\inl {x_1})}}   
+            \end{stackTL}
+            \\
+          & &  \mid {x_2'.
+              \begin{stackTL}
+              \bindXtoYinZ{(\dncast{\u F A_2}{\u F A_2'}{(\ret{x_2'})})}{x_2}\\{\ret{(\inr {x_2})}}  
+              \end{stackTL}
+              } \}\\
+        \end{array}
+        \\\\
+        \upcast{A_1 \times A_2}{A_1' \times A_2'}{p} \equidyn \pmpairWtoXYinZ{p}{x_1}{x_2}{(\upcast{A_1}{A_1'}{x_1},\upcast{A_2}{A_2'}{x_2})} \\\\
+        \begin{array}{rcl}
+          \dncast{\u F (A_1' \times A_2')}{\u F (A_1 \times A_2)}{\bullet} &
+          \equidyn & 
+          \bindXtoYinZ{\bullet}{p'} {\pmpairWtoXYinZ{p'}{x_1'}{x_2'}{}}\\
+          & & \bindXtoYinZ{\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}{x_1}\\
+          & & \bindXtoYinZ{\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}{x_2} {\ret (x_1,x_2) }\\\\
+          & \equidyn &  
+          \bindXtoYinZ{\bullet}{p'} \pmpairWtoXYinZ{p'}{x_1'}{x_2'}{} \\
+          & & \bindXtoYinZ{\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}{x_2} \\
+          & & \bindXtoYinZ{\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}{x_1} {\ret (x_1,x_2) }
+        \end{array}\\\\
+        %% if losing space due to not pagebreaking in the middle of this
+        %%     \\\\
+        %%   \end{array}
+        %% \]
+        %% \[
+        %%   \begin{array}{c}
+
+        \dncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}{\bullet} \equidyn 
+        \pair{\dncast{\u B_1}{\u B_1'}{\pi \bullet}}{\dncast{\u B_2}{\u B_2'}{\pi' \bullet}}\\\\
+        \begin{stackTL}
+        \upcast{U (\u B_1 \with \u B_2)}{U (\u B_1' \with \u B_2')}{p}\\
+        \quad\equidyn \thunk{}
+          \begin{stackTL}
+            {\{\pi \mapsto {\force{(\upcast{U \u B_1}{U \u B_1'}{(\thunk{\pi (\force{p})})})}}}\\
+            \,\,|\,\,\pi' \mapsto {\force{(\upcast{U \u B_2}{U \u B_2'}{(\thunk{\pi' (\force{p})})})}}
+          \end{stackTL}          
+           \}
+        \end{stackTL}
+
+        \\\\
+        \dncast{A \to \u B}{A' \to \u B'}{\bullet} \equidyn
+        \lambda{x}.{\dncast{\u B}{\u B'}{(\bullet \, (\upcast{A}{A'}{x}))}} \\\\
+
+        \upcast{U (A \to \u B)}{U (A' \to \u B')}{f} \equidyn
+        \thunk (\lambda x'.
+        \begin{stackTL}
+          \bindXtoYinZ{\dncast{\u F A}{\u F A'}{(\ret x')}}{x}{} \\
+          { \force{(\upcast{U \u B}{U \u B'}{(\thunk{(\force{(f)}\,x)})})}}
+        \end{stackTL}
+      \end{array}
+      \]
+    \end{footnotesize}
+    \caption{Derivable Cast Behavior for $+,\times,\with,\to$}
+    \label{fig:uniq-impl}
+  \end{figure}
 \end{theorem}
+
 In the case for an eager product $\times$, we can actually also show
 that reversing the order and running ${\dncast{\u F A_2}{\u F A_2'}{\ret
     x_2'}}$ and then ${\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}$ is also
@@ -3257,42 +3281,33 @@ such:
   ${x \ltdyn x' : A \ltdyn A' \vdash x \ltdyn \defdncast{A}{A'} x' : A}$.
 \end{enumerate}
 \end{definition}
-\begin{longonly}
 Because the proofs of Lemma~\ref{lem:cast-left-right},
 Lemma~\ref{lem:cast-congruence}, Theorem~\ref{thm:decomposition},
 Theorem~\ref{thm:casts-unique} rely only on the axioms for
 upcasts/downcasts, the analogues of these theorems hold for stack
 upcasts and value downcasts as well.
-\end{longonly}
+
+TODO: move this stuff earlier to the defined upcast/downcast section
 Some value downcasts and computation upcasts do exist, leading to a
 characterization of the casts for the monad $U \u F A$ and comonad $\u F
 U \u B$ of $F \dashv U$:
 \begin{theorem}[Cast Unique Implementation Theorem for $U \u F, \u F U$] \label{thm:monadic-comonadic-casts}
   Let $A \ltdyn A'$ and $\u B \ltdyn \u B'$.  
   \begin{enumerate}
-  \item $\bullet : \u F A \vdash
-    \bindXtoYinZ{\bullet}{x:A}{\ret{(\upcast{A}{A'}{x})}} : \u F A'$
-    is a stack upcast.
+  %% \item $\bullet : \u F A \vdash
+  %%   \bindXtoYinZ{\bullet}{x:A}{\ret{(\upcast{A}{A'}{x})}} : \u F A'$
+  %%   is a stack upcast.
     
-  \item If $\defupcast{\u B}{\u B'}$ is a stack upcast, then\\
-    $x : \u U B \vdash \upcast{U \u B}{\u U B'}{x} \equidyn \thunk{(\defupcast{\u B}{\u B'}{(\force x)})} : U \u B'$
+  \item $x : U \u F A \vdash \upcast{U \u F A}{\u U B'}{x} \equidyn \thunk{(\defupcast{\u F A}{\u F A'}{(\force x)})} : U \u F A'$
     
-  \item $x : \u U B' \vdash \thunk{(\dncast{\u B}{\u B'}{(\force x)})} : U
-    \u B$ is a value downcast.
+  %% \item $x : \u U B' \vdash \thunk{(\dncast{\u B}{\u B'}{(\force x)})} : U
+  %%   \u B$ is a value downcast.
     
-  \item If $\defdncast{A}{A'}$ is a value downcast, then\\
-    $\bullet : \u F A' \vdash \dncast{\u F A}{\u F A'}{\bullet} \equidyn \bindXtoYinZ{\bullet}{x':A'}{\ret{(\dncast{A}{A'}{x})}}$
-
-  \item 
-    $\begin{array}{c}
-    x : U \u F A \vdash \upcast{U \u F A}{U \u F A'}{x} \equidyn \thunk{ (\bindXtoYinZ{{\force x}}{x:A}{\ret{(\upcast{A}{A'}{x})}})}\\
-    \bullet : \u F U \u B' \vdash \dncast{\u F U \u B}{\u F U \u B'}{\bullet} \equidyn
-    \bindXtoYinZ{\bullet}{x':U \u B'}{\ret{(\thunk{(\dncast{\u B}{\u B'}{(\force x)})})}}
-    \end{array}$
+  \item $\bullet : \u F U \u B' \vdash \dncast{\u F U \u B}{\u F U \u B'}{\bullet} \equidyn \bindXtoYinZ{\bullet}{x':U \u B'}{\ret{(\dncast{U \u B}{U \u B'}{x})}}$
   \end{enumerate}
 \end{theorem}
-
 \begin{longproof}
+  TODO: update the proof
   \begin{enumerate}
   \item
     To show
@@ -3402,6 +3417,7 @@ U \u B$ of $F \dashv U$:
   \end{enumerate}
 \end{longproof}
 
+TODO: make this whole thing a forward reference to the CBV section
 \begin{longonly}
   \subsubsection{Derived Rules for Call-by-value Function Types}
 \end{longonly}
@@ -3461,10 +3477,16 @@ let-bind $(\upcast{A_1}{A_1'}{x})$ to avoid duplicating it, but because
 it is a (complex) value, it can also be substituted directly, which
 might expose reductions that can be optimized.
 
-\begin{longonly}
 \subsection{Least Dynamic Types}
 
-\begin{longonly}
+Though it is common in gradually typed surface languages to have a
+\emph{most} dynamic type in the form of the dynamic type $\dyn$, it is
+less common to have a \emph{least} dynamic type. We consider here the
+\emph{semantic} impliciations of having a least dynamic value or
+computation type. Perhaps unsurprisingly, we find that a least dynamic
+type must be isomorphic to $0$ and a least dynamic computation type
+must be isomorphic to $\top$.
+
 \begin{theorem}[Least Dynamic Value Type]
   If $\leastdynv$ is a type such that $\leastdynv \ltdyn A$ for all $A$,
   then in GTT with a strict initial object $0$, $\leastdynv \cong_{v}
@@ -3484,7 +3506,7 @@ If $\leastdync$ is a type such that $\leastdync \ltdyn \u B$ for all $\u
 B$, and we have a terminal computation type $\top$, then $U \leastdync
 \cong_{v} U \top$.
 \end{theorem}
-\begin{proof}
+\begin{longproof}
 We have stacks $\bullet : \top \dncast{\leastdync}{\top}{\bullet} :
 \leastdync$ and $\bullet : \leastdync \vdash \{\} : \top$.  The
 composite at $\top$ is the identity by Lemma~\ref{lem:terminal}.  However,
@@ -3504,10 +3526,9 @@ and the composite
 y : U \top \vdash \upcast{U \leastdync}{U \top}{(\thunk{(\dncast{\leastdync}{\top}{(\force{x})})})} : U \top
 \]
 is the identity by uniqueness for $U \top$ (Lemma~\ref{lem:terminal}).  
-\end{proof}
+\end{longproof}
 
 This suggests taking $\bot_v := 0$ and $\bot_c := \top$.
-\end{longonly}
 
 %% \begin{shortonly}
 %% The dynamic types are the \emph{most} dynamic types; it is interesting
@@ -3588,7 +3609,6 @@ Dually, the casts determined by $\top \ltdyn \u B$ are
     B$ gives the result.
   \end{enumerate}
 \end{longproof}
-\end{longonly}
 
 \subsection{Upcasts are Values, Downcasts are Stacks}
 \label{sec:upcasts-necessarily-values}
-- 
GitLab