diff --git a/paper/gtt.tex b/paper/gtt.tex
index ae21b627a2411f1e591394ade0f345bab3780ddb..608974c7d9ec19b1306a2bd3dbe7db13a40a3fc2 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -4417,31 +4417,48 @@ Section~\ref{sec:upcasts-necessarily-values} \emph{with $0$ and $\top$ removed},
   compositionally otherwise.
 \end{definition}
 
-
-Next, we show several possible interpretations of the dynamic type that
-will all give, by construction, implementations that satisfy the gradual
-guarantee.
+Next, we show several possible interpretations of the dynamic type
+that will all give, by construction, implementations that satisfy the
+gradual guarantee.
+%
+Our interpretations of the value dynamic type are not surprising.
+%
+They are the usual construction of the dynamic type using type tags:
+i.e., a recursive sum of basic value types.
+%
+On the other hand, our interpretations of the computation dynamic type
+are less familiar.
+%
+In duality with the interpretation of $\dynv$, we interpret $\dync$ as
+a recursive \emph{product} of basic computation types.
+%
+This interpretation has some analogues in previous work on the duality
+of computation \citep{girard01locussolum,zeilberger09thesis}, but the
+most direct interpretation (definition \ref{def:natural-type-interp})
+does not correspond to any known work on dynamic/gradual typing.
+%
+Then we show that a particular choice of which computation types is
+basic and which are derived produces an interpretation of the dynamic
+computation type as a type of variable-arity functions whose arguments
+are passed on the stack, producing a model similar to Scheme without
+accounting for control effects (definition
+\ref{def:scheme-like-type-interp}).
 
 \subsubsection{Natural Dynamic Type Interpretation}
 
-Our first dynamic type interpretation simply constructs recursive types
-supporting the required ep pairs.  
+Our first dynamic type interpretation is to make the value and
+computation dynamic types sums and products of the ground value and
+computation types, respectively.
+%
+This forms a model of GTT for the following reasons.
 %
 For the value dynamic type $\dynv$, we need a value embedding (the
 upcast) from each ground value type $G$ with a corresponding projection.
 %
 The easiest way to do this would be if for each $G$, we could rewrite
 $\dynv$ as a sum of the values that fit $G$ and those that don't:
-$\dynv \cong G + \dynv_{-G}$ because 
+$\dynv \cong G + \dynv_{-G}$ because of the following lemma.
 
-\begin{longonly}
-  \begin{lemma}[$\u F(+)$ Induction Principle]
-  $\Gamma\pipe \cdot : \u F (A_1 + A_2) \vdash M_1 \ltdyn M_2 : \u B$
-  holds if and only if
-  $\Gamma, V_1: A_1 \vdash M_1[\ret \inl V_1] \ltdyn M_2[\ret \inl V_2] : \u B$ and
-  $\Gamma, V_2: A_2 \vdash M_2[\ret \inr V_2] \ltdyn M_2[\ret \inr V_2] : \u B$ 
-\end{lemma}
-\end{longonly}
 \begin{lemma}[Sum Injections are Value Embeddings]\label{lem:injections-are-embeddings}
   For any $A, A'$, there are value ep pairs from $A$ and $A'$ to
   $A+A'$ where the embeddings are $\inl$ and $\inr$.
@@ -4451,7 +4468,7 @@ $\dynv \cong G + \dynv_{-G}$ because
   projection to be $\bindXtoYinZ \bullet y \caseofXthenYelseZ y {\inl x. \ret
     x}{\inr _. \err}$.
   \begin{longonly}
-    This satisfies retraction (using $\u F(+)$ induction, $\inr$ case is the same):
+    This satisfies retraction (using $\u F(+)$ induction (lemma \ref{lem:f-induction}), $\inr$ case is the same):
     \begin{align*}
       \bindXtoYinZ {\inl x} y \caseofXthenYelseZ y {\inl x. \ret x}{\inr _. \err}
       &\equidyn \caseofXthenYelseZ {\inl x} {\inl x. \ret x}{\inr _. \err}\tag{$\u F\beta$}\\
@@ -4469,13 +4486,24 @@ $\dynv \cong G + \dynv_{-G}$ because
     \end{align*}
   \end{longonly}
 \end{proof}
+\begin{longonly}
+  Whose proof relies on the following induction principle for the
+  returner type:
+  \begin{lemma}[$\u F(+)$ Induction Principle]
+    \label{lem:f-induction}
+  $\Gamma\pipe \cdot : \u F (A_1 + A_2) \vdash M_1 \ltdyn M_2 : \u B$
+  holds if and only if
+  $\Gamma, V_1: A_1 \vdash M_1[\ret \inl V_1] \ltdyn M_2[\ret \inl V_2] : \u B$ and
+  $\Gamma, V_2: A_2 \vdash M_2[\ret \inr V_2] \ltdyn M_2[\ret \inr V_2] : \u B$ 
+\end{lemma}
+\end{longonly}
 
-Therefore, it is very natural to make the dynamic type the minimal type
-with injections from each $G$: i.e., the sum of all value ground types
-$? \cong \Sigma_{G} G$.
+This shows why the type tag interpretation works: it makes the dynamic
+type in some sense the minimal type with injections from each $G$:
+the sum of all value ground types $? \cong \Sigma_{G} G$.
 
-The dynamic computation type $\dync$ can be naturally defined by a dual
-construction.
+The dynamic computation type $\dync$ can be naturally defined by a
+dual construction, by the following dual argument.
 %
 First, we want a computation ep pair from $\u G$ to $\dync$ for each
 ground computation type $\u G$.
@@ -4490,7 +4518,8 @@ other behaviors'', i.e., $\dync \cong \u G \with \dync_{-\u G}$.
 Then the embedding on $\pi$ performs the embedded computation, but on
 $\pi'$ raises a type error.
 %
-The following lemma shows this forms a computation ep pair:
+The following lemma, dual to lemma \ref{lem:injections-are-embeddings}
+shows this forms a computation ep pair:
 
 \begin{lemma}[Lazy Product Projections are Computation Projections]\label{lem:projections-are-projections}
   For any $\u B, \u B'$, there are computation ep pairs from $\u B$
@@ -4522,11 +4551,12 @@ The following lemma shows this forms a computation ep pair:
 From this, we see that the easiest way to construct an interpretation
 of the dynamic computation type is to make it a lazy product of all
 the ground types $\u G$: $\dync \cong \With_{\u G} \u G$.
-
+%
 Using recursive types, we can easily make this a definition of the
 interpretations:
 
 \begin{definition}[Natural Dynamic Type Interpretation]
+  \label{def:natural-type-interp}
   The following defines a dynamic type interpretation.
   %
   We define the types to satisfy the isomorphisms
@@ -4662,10 +4692,10 @@ type is booleans $1+1$), we can restrict the dynamic types as follows:
 
 \subsubsection{Scheme-like Dynamic Type Interpretation}
 
-However, the above dynamic type interpretation does not correspond to
-any known dynamically typed language, in part because it includes
-explicit cases for the ``additives'', the sum type $+$ and lazy product
-type $\with$.
+The above dynamic type interpretation does not correspond to any
+dynamically typed language used in practice, in part because it
+includes explicit cases for the ``additives'', the sum type $+$ and
+lazy product type $\with$.
 %
 Normally, these are not included in this way, but rather sums are
 encoded by making each case use a fresh constructor (using nominal