diff --git a/paper/gtt.tex b/paper/gtt.tex
index 45a29e2bb66a22d0ec0fa57d94544a907621dd01..49e4d7e2f0839c4643f235c4d5c975f54b16f43a 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -191,7 +191,7 @@
 \newcommand{\thunk}{\kw{thunk}}
 \newcommand{\force}{\kw{force}}
 \newcommand{\abort}{\kw {abort}}
-\newcommand{\with}{\mathop{\&}}
+\newcommand{\with}{\mathbin{\&}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{document}
@@ -767,16 +767,11 @@ translation, but we leave this to future work.
 In particular the aim of this section is to establish the following
 theorems:
 
-\begin{theorem}{Consistency of GTT}
-  There exists a judgment $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn
-  M_2 : B_1 \ltdyn B_2$ that is not provable.
-\end{theorem}
-
-\begin{theorem}{Contextual Approximation}
+\begin{theorem}{Graduality}
   If $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn M_2 : B_1 \ltdyn
-  B_2$, then for any context $C : (\Gamma_1 \vdash B_1) \Rightarrow
-  (\cdot \vdash \u F 2)$, and any valid interpretation of the dynamic
-  types, one of the following holds
+  B_2$, then for any GTT context $C : (\Gamma_1 \vdash B_1)
+  \Rightarrow (\cdot \vdash \u F 2)$, and any valid interpretation of
+  the dynamic types, one of the following holds
   \begin{enumerate}
   \item $\sem{C[M_1]} \Downarrow \err$
   \item $\sem{C[M_1]}, \sem{C[\dncast{B_1}{B_2}M_2[\upcast{\Gamma_1}{\Gamma_2}{\Gamma_1}]]} \Uparrow$
@@ -786,6 +781,17 @@ theorems:
   \end{enumerate}
 \end{theorem}
 
+As a consequence we get the consistency of the type theory:
+\begin{corollary}{Consistency of GTT}
+  There exists a judgment $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn
+  M_2 : B_1 \ltdyn B_2$ that is not provable.
+\end{corollary}
+\begin{proof}
+  $\ret \tru \ltdyn \ret \fls$ is not provable since they are
+  distinguished by the empty context.
+\end{proof}
+
+
 As described in the previous section, almost all of the contract
 translation is uniquely determined already: casts between function
 types must wrap inputs and outputs, pairs cast each component, etc.
@@ -930,13 +936,75 @@ on the other tags.
   We 
 \end{proof}
 
-The inclusion of sums, and negative products as tags on the dynamic
-type is uncommon in dynamically typed languages.
+The inclusion of sums, and negative products as primitives is uncommon
+in dynamically typed languages.
+%
+Instead, sums are usually encoded using a kind of fresh atomic values
+to distinguish between different constructors, i.e. using
+\emph{nominal} features.
+%
+Treating this fresh generation of values is out of scope for this
+current paper.
+
+However, a sum injection $\sigma_{1} V$ can also be encoded using
+a pair of a boolean and the value $V$: $(1, V)$.
+%
+This is for example used in minimalist dialects of Scheme and Lisp,
+where rather than a boolean value, a \emph{symbol} that has an
+informative name is used.
+%
+The next interpretation we present is based on this idea.
+%
+The dynamic value type is the type of binary trees whose leaves are
+booleans or (opaque) closures, which we can think of as a basic type
+of S-expressions.
+%
+We define this in the standard way as a recursive type $\mu X. (1 + 1)
++ U\dync + (X \times X)$.
+
+The dynamic computation type looks a bit strange at first: it is
+defined as a lazy pair of a function $\dynv \to \dync$ and a returner
+$\u F \dynv$.
+%
+However, consider its infinite unfolding:
+\[ (\u F \dynv) \with (\dynv \to \u F \dynv) \with (\dynv \to \dynv \to \u F \dynv) \with \cdots \]
+%
+Taking the session-typing view that a lazy product is a selection of
+options for a consumer, this says that the consumer can \emph{call}
+the function with any number of arguments pushed onto the stack.
 %
-Instead, sums can be encoded using a pair of some atomic enumeration
-type and the payload.
+We observe that this is isomorphic to the more common type: $\dynv^*
+\to \u F \dynv$ where $A^* = \mu X. 1 + (A \times X)$ is the type of
+finite lists, which we can prove as follows:
+\begin{align*}
+  &(\u F \dynv) \with (\dynv \to \u F \dynv) \with (\dynv \to \dynv \to \u F \dynv) \with \cdots\\
+  &\cong (1 \to \u F \dynv) \with (\dynv \times 1 \to \u F \dynv) \with (\dynv \times (\dynv \times 1) \to \u F \dynv) \with \cdots\\
+  &\cong (1 + (\dynv \times 1) + (\dynv \times \dynv \times 1) + \cdots) \to \u F \dynv\\
+  &\cong (\mu X. 1 + (\dynv \times X)) \to \u F \dynv\\
+  &= \dynv^* \to \u F \dynv
+\end{align*}
+%
+However, operationally, our definition as a recursive computation type
+is more true to the implementation of Scheme-like languages, where
+multi-argument function application simply pushes all of the arguments
+onto the stack.
+%
+The type $\dynv^* \to \u F \dynv$ on the other hand corresponds to an
+implementation that constructs a cons-list and then passes it as a
+single argument on the stack.
+%
+The introduction form of this language corresponds to something very
+much like Scheme's ``case-lambda'' operator for defining
+multi-argument functions.
+
+Thinking of $\with$ as a kind of constructor for objects, we can think
+of a term of type $\dync$ as representing an object with one method
+for every natural number that takes that many S-expressions and
+returns an S-expression.
 %
-The next interpreation we present is based on this idea.
+In other words, this interpretation of $\dync$ says that all
+computations in GTT can be implemented as \emph{variable-arity
+  multi-argument functions}, another 
 %
 We use booleans as the atomic enumeration for simplicity, but we could
 of course use some larger type of machine integers in an
@@ -951,10 +1019,10 @@ pairs are interpreted as a sigma type and functions as a pi type.
 In addition, we can drop the $1$ case by interpreting it as one of the
 booleans.
 
-\begin{definition}[Sums-as-pairs Dynamic Type Interpretation]
+\begin{definition}[Scheme-like Dynamic Type Interpretation]
   The following defines a dynamic type interpretation.
   \begin{align*}
-    \rho(\dynv) &= (1 + 1) + (\rho(\dynv) \times \rho(\dynv)) + U\rho(\dync) \\
+    \rho(\dynv) &= (1 + 1) + U\rho(\dync) + (\rho(\dynv) \times \rho(\dynv)) \\
     \rho(\dync) &= (\rho(\dynv) \to \rho(\dync)) \with \u F \rho(\dynv)
   \end{align*}
   and define for each $G$,
@@ -1350,6 +1418,8 @@ Next, we give the inequational theory for our CBPV language.
 \subsection{Graduality Logical Relation}
 
 
+
+
 \begin{figure}
   \begin{mathpar}
     {\logty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2 \quad\qquad{\logty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\quad\qquad {\logc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\
@@ -1395,6 +1465,7 @@ Next, we give the inequational theory for our CBPV language.
     \ipole \omega M_3$ then $M_1 \ipole i M_3$.
 
     % TODO: might as well make error the least element? not sure
+
   \item Error awareness: For all $i \in \nats$, $\err \ipole i \err$.
   \end{enumerate}
 \end{definition}
@@ -1839,7 +1910,11 @@ with errors, in order to efficiently arrive at a concrete operational
 interpretation.
 %
 It may be of interest to develop a more general notion of model of GTT
-for which we can prove soundness and completeness theorems.
+for which we can prove soundness and completeness theorems, as in
+\cite{cbn-gtt}.
+%
+
+
 %
 Furthermore, the ordered CBPV with errors should also have a sound and
 complete notion of model, and so our contract translation should have
@@ -1880,6 +1955,14 @@ This gives some evidence that the specific choice of connectives of
 CBPV occupies a certain ``sweet spot'' between semantic expressivity
 and amenability to extensions.
 
+\paragraph{Dynamically Typed Call-by-push-value}
+
+Our interpretation of the dynamic types in CBPV suggests a design for
+a Scheme-like language with a value and computation distinction.
+%
+This may be of interest for designing an extension of Type Racket that
+efficiently supports CBN or a scheme-like language with codata types.
+
 \appendix
 
 In this appendix we present for the reader who is unfamiliar with