diff --git a/paper/gtt.tex b/paper/gtt.tex
index 1ee325d172cbf8065f7139f195bdce14029c8e00..210f60cbcdca9cbcfe08cb8ab46346c5294717a8 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1023,6 +1023,14 @@ lemmas, and proofs.
 \section{Axiomatic Gradual Type Theory}
 \label{sec:gtt}
 
+In this section we introduce the syntax of Gradual Type Theory, an
+extension of Call-by-push-value to support the constructions of
+gradual typing.
+%
+First we introduce call-by-push-value and then describe in turn the
+gradual typing features: dynamic types, casts, and the dynamism
+orderings on types and terms.
+
 \begin{figure}
   \begin{small}
   \[
@@ -9335,15 +9343,50 @@ casts~\cite{siekwadler10zigzag}, are equivalent to the lazy contract
 semantics, they should also be models of GTT, and if so we could use GTT
 to reason about program transformations and optimizations in them.
 
-We plan to use this core calculus as a target language for multiple
-high level gradually typed languages, with the high-level languages
-inheriting proofs of graduality and appropriate forms of $\eta$
-equivalence.
+\iflong
+\paragraph{Applicability of Cast Uniqueness Principles}
+\fi
+
+The cast uniqueness principles given in theorem
+\ref{thm:functorial-casts} are theorems in the logic of Gradual Type
+Theory, so there is a question of what languages the theorem applies
+to.
+%
+The theorem applies to any \emph{model} of gradual type theory, such
+as the models given in sections \ref{sec:contract}, \ref{sec:complex},
+\ref{sec:operational}.
+%
+We argue that this applies directly to languages that are
+call-by-value and call-by-name, not just call-by-push-value itself.
 %
-We have focused on the application to call-by-value source languages
-because almost all work on gradually typed languages has taken place
-in a call-by-value setting.
+TODO: why
+
+Finally, we note that the case of the theorem for function types does
+\emph{not} apply to call-by-value languages where the restricetd
+$\eta$ principle for functions is not satisfied. In particular
+languages where functions can be tested for pointer equality. It is a
+well-known issue that the lazy semantics of functions and objects is
+not valid in the presence of pointer equality (TODO: cite semantic
+casts) and our uniqueness theorem provides a different perspective on
+this result.
+
+%
+However, we note that the cases of the theorem are completely
+\emph{modular} in that the proof for any individual connective
+$\to,\times,\ldots$ only relies on the $\eta$ principle for that
+connective.
+%
+This means that the case of the theorem for a particular connective
+applies to any model of any \emph{subsystem} of GTT that includes the
+$\eta$ principle for that connective.
+%
+For instance, if $\times\eta$ holds, then the product cast uniqueness
+theorem is provable, whether or not a dynamic computation type $\dync$
+is assumed to exist, or the $\to\eta$ principle holds.
+
 
+% TODO: the following is all subsumed by using Levy's account of
+% "the lazy paradigm"
 While call-by-value evaluation is a fairly consistent notion,
 non-eager evaluation comes in many flavors.
 %
@@ -9448,7 +9491,7 @@ More specifically, many of the lemmas proven in the extended version
 of the paper have direct analogues in Henglein's work.
 %
 We have not included these lemmas in the paper because they are quite
-similar to lemmas proven in \citet{newahmed18}, and see there for a
+similar to lemmas proven in \citet{newahmed18}; see there for a
 more detailed comparison.
 %
 Finally, we note that our assumption of compositionality, i.e., that
@@ -9461,9 +9504,9 @@ coercion calculus.
 \fi
 
 Our approach to systematically producing a gradual type theory from a
-type theory is similar in spirit to ``frameworks'' for gradual typing,
-specifically AGT \cite{AGT} and the Gradualizer
-\cite{gradualizer16,gradualizer17}.
+type theory by adding dynamic types, casts and dynamism orderings is
+similar in spirit to ``frameworks'' for gradual typing, specifically
+AGT \cite{AGT} and the Gradualizer \cite{gradualizer16,gradualizer17}.
 %
 These two frameworks systematically produce a gradual language from a
 statically typed language, and both produce a surface language with a
@@ -9476,9 +9519,8 @@ statically typed language, whereas our approach is to ``gradualize''
 the axiomatic semantics of the typed language.
 %
 This means our approach accomplishes something quite different: their
-frameworks produce specific implementations, whereas GTT (without
-$\eta$ principles) axiomatizes the commonalities across different
-implementations.
+frameworks produce specific implementations, whereas GTT axiomatizes
+the commonalities across different implementations.
 % AA: Perhaps the above point should also be made in the intro. 
 Furthermore, while both the AGT and Gradualizer approaches prove various
 gradual typing correctness theorems by construction (gradual type