diff --git a/paper/gtt.tex b/paper/gtt.tex
index fc462a2412428940d97b8071ed45db0756fef516..95b98ea53a0b65d53889860aa17daa4bd693e88e 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1040,24 +1040,29 @@ A_2$), and expressions that pattern-match on values (e.g. $p : A_1
 A_1$).  Thus, the complex values $x : A \vdash V : A'$ are a syntactic
 class of ``pure functions'' from $A$ to $A'$ (though there is no pure
 function \emph{type} internalizing this judgement), which can be treated
-like values by a compiler (e.g. they can duplicated, reordered,
-common-subexpression-eliminated because they have no effects).  In
+like values by a compiler because they have no effects (e.g. they can be
+dead-code-eliminated, common-subexpression-eliminated, and so on).  In
 focusing~\cite{andreoli,something-intuitionistic} terms, complex values
-consist of left inversion and right focus rules.  Complex values can be
-eliminated in favor of only allowing pattern-matching in computations
-(see Section~\ref{sec:complex}), but we use them to simplify the
-presentation of our results about casts.  For each pattern-matching
-construct (case analysis on a sum, splitting a pair), we have both an
-elimination rule whose branches are values
+consist of left inversion and right focus rules.  For each
+pattern-matching construct (e.g. case analysis on a sum, splitting a
+pair), we have both an elimination rule whose branches are values
 (e.g. $\caseofXthenYelseZ{s}{x_1.V_1}{x_2.V_2}$) and one whose branches
 are computations (e.g. $\caseofXthenYelseZ{s}{x_1.M_1}{x_2.M_2}$).  To
 abbreviate the typing rules for both in
-Figure~\ref{fig:gtt-syntax-and-terms}, we use the following
-convention: we write $E$ for either a complex value or a computation,
-and $T$ for either a value type $A$ or a computation type $\u B$, and a
-judgement $\Gamma \mid \Delta \vdash E : T$ for either $\Gamma \vdash V
-: A$ or $\Gamma \mid \Delta \vdash M : \u B$ (this is a bit of an abuse
-of notation because $\Delta$ is not present in the former).
+Figure~\ref{fig:gtt-syntax-and-terms}, we use the following convention:
+we write $E$ for either a complex value or a computation, and $T$ for
+either a value type $A$ or a computation type $\u B$, and a judgement
+$\Gamma \mid \Delta \vdash E : T$ for either $\Gamma \vdash V : A$ or
+$\Gamma \mid \Delta \vdash M : \u B$ (this is a bit of an abuse of
+notation because $\Delta$ is not present in the former).
+
+Complex values can be translated away without loss of expressiveness by
+moving all pattern-matching into computations (see
+Section~\ref{sec:complex}), because in CBPV without complex values,
+there is a behavioral condition of \emph{thunkability}~\cite{gmm} that
+captures the property complex values have. However, we find it simpler
+to present our results about casts using complex values than using
+thunkable computations.  
 
 \paragraph{Shifts}
 A key notion in CBPV is the \emph{shift} types $\u F A$ and $U \u B$,
@@ -1069,19 +1074,20 @@ type $A$ (\ret{V}), while the elimination rule is sequencing a
 computation of an $\u F A$ with a computation $x : A \vdash M : \u B$ to
 produce a computation of a $\u B$ ($\bindXtoYinZ{M}{x}{N}$).  While any
 closed complex value $V$ is equivalent to an actual value, a computation
-of type $\u F A$ might perform other effects (e.g. printing) before
-returning a value, or might error or non-terminate and not return a
-value at all.  The introduction and elimination rules for $U$ are
-written $\thunk{M}$ and $\force{V}$, and say that computations of type
-$\u B$ are bijective with values of type $U \u B$.  For example, $0$ is
-the empty value type, so $\u F 0$ classifies effectful computations that
-never return, but may perform effects (and then, must e.g. non-terminate
-or error), while $U \u F 0$ is the value type where such computations
-are thunked/delayed and considered as values.  $1$ is the trivial value
-type, so $\u F 1$ is the type of computations that can perform effects
-with the possibility of terminating successfully by returning $()$, and
-$U \u F 1$ is the value type where such computations are delayed values.
-$U \u F$ is a monad on value types~\citep{moggi}.
+of type $\u F A$ might perform effects (e.g. printing) before returning
+a value, or might error or non-terminate and not return a value at all.
+The introduction and elimination rules for $U$ are written $\thunk{M}$
+and $\force{V}$, and say that computations of type $\u B$ are bijective
+with values of type $U \u B$.  As an example of the action of the
+shifts, $0$ is the empty value type, so $\u F 0$ classifies effectful
+computations that never return, but may perform effects (and then, must
+e.g. non-terminate or error), while $U \u F 0$ is the value type where
+such computations are thunked/delayed and considered as values.  $1$ is
+the trivial value type, so $\u F 1$ is the type of computations that can
+perform effects with the possibility of terminating successfully by
+returning $()$, and $U \u F 1$ is the value type where such computations
+are delayed values.  $U \u F$ is a monad on value types~\citep{moggi},
+while $\u F U$ is a comonad on computation types.  
 
 \paragraph{Computation types}
 The computation type constructors in CBPV include lazy unit/products
@@ -1089,49 +1095,48 @@ $\top$ and $\u B_1 \with \u B_2$, which behave as in a call-by-name/lazy
 language (e.g. a component of a lazy pair is evaluated only when it is
 projected).  Functions $A \to \u B$ have a value type as input and a
 computation type as a result.  The equational theory of effects in CBPV
-computations may at first be a bit surprising to those familiar with
+computations may at first be surprising to those familiar with
 call-by-value, because at higher computation types effects have a
 call-by-name-like equational theory.  For example, at computation type
 $A \to \u B$, we have an equality $\print c; \lambda x. M = \lambda
-x.\print c; M$.  Intuitively, the reason is that $A \to \u B$ is not
+x.print c; M$.  Intuitively, the reason is that $A \to \u B$ is not
 treated as an \emph{observable} type (one where computations are run):
 the states of the operational semantics are only those comptuations of
 type $\u F A$ for some value type $A$.  Thus, ``running'' a function
 computation means supplying it with an argument, and applying both of
-the above to an argument $V$ is defined to result in $\print c;M[V/x]$.
+the above to an argument $V$ is defined to result in $print c;M[V/x]$.
 This does \emph{not} imply that the corresponding equations holds for
 the call-by-value function type, which we discuss below.  As another
 example, \emph{all} computations are considered equal at type $\top$,
-even computations that look manifestly different ($\print 'a'$
-vs. $\{\}$ vs. $\err$), because there is by definition \emph{no} way to
-extract an observable of type $\u F A$ from a computation of type
-$\top$.  Consequently, $U \top$ is isomorphic to $1$, because it is also
-a value type with exactly one element.
+even computations that perform different effects ($\print c$ vs. $\{\}$
+vs. $\err$), because there is by definition \emph{no} way to extract an
+observable of type $\u F A$ from a computation of type $\top$.
+Consequently, $U \top$ is isomorphic to $1$.
 
 \paragraph{Complex stacks}
 Just as the complex values $V$ are a syntactic class terms that have no
-effects, CBPV includes a judgement for \emph{stacks} $S$, a syntactic
-class of terms that reflect \emph{all} effects of their input.  A
-\emph{stack} $\Gamma \mid \bullet : \u B \vdash S : \u B'$ can be
-thought of as a linear/strict function from $\u B$ to $\u B'$, which
-\emph{must} use its input hole $\bullet$ \emph{exactly} once.
-Consequently, stacks satisfy a number of equations that are useful for
-refactorings or in a compiler: effects can be hoisted out of stacks,
-because we know the stack will run them exactly once.  For example, we
-can have a contextual equivalence $S[\err/\bullet] = \err$ and $S[\print
-  V;M] = \print V;S[M/\bullet]$.  Just as complex values include
-pattern-matching, \emph{complex stacks} include pattern-matching on
-values and introduction forms for the stack's output type.  For example,
-$\bullet : \u B_1 \with \u B_2 \vdash \pair{\pi' \bullet}{\pi \bullet} :
-\u B_2 \with \u B_1$ is a complex stack, even though it mentions
-$\bullet$ more than once, because running the computation requires
-choosing a projection to get to an observable of type $\u F A$, so
-\emph{each time it is run} it uses $\bullet$ exactly once.  In focusing
-terms, complex stacks include both left and right inversion, and left
-focus rules.  In the equational theory of CBPV, $\u F$ and $U$ are
-\emph{adjoint}, in the sense that stacks $\bullet : \u F A \vdash S : \u
-B$ are bijective with values $x : A \vdash V : U \u B$, as both are
-bijective with computations $x : A \vdash M : \u B$.
+effects, CBPV includes a judgement for ``stacks'' $S$, a syntactic class
+of terms that reflect \emph{all} effects of their input.  A \emph{stack}
+$\Gamma \mid \bullet : \u B \vdash S : \u B'$ can be thought of as a
+linear/strict function from $\u B$ to $\u B'$, which \emph{must} use its
+input hole $\bullet$ \emph{exactly} once.  Consequently, stacks satisfy
+equations that are useful for refactorings or in a compiler: effects can
+be hoisted out of stacks, because we know the stack will run them
+exactly once.  For example, there will be contextual equivalences
+$S[\err/\bullet] = \err$ and $S[\print V;M] = \print V;S[M/\bullet]$.
+Just as complex values include pattern-matching, \emph{complex stacks}
+include pattern-matching on values and introduction forms for the
+stack's output type.  For example, $\bullet : \u B_1 \with \u B_2 \vdash
+\pair{\pi' \bullet}{\pi \bullet} : \u B_2 \with \u B_1$ is a complex
+stack, even though it mentions $\bullet$ more than once, because running
+the computation requires choosing a projection to get to an observable
+of type $\u F A$, so \emph{each time it is run} it uses $\bullet$
+exactly once.  In focusing terms, complex stacks include both left and
+right inversion, and left focus rules.  In the equational theory of
+CBPV, $\u F$ and $U$ are \emph{adjoint}, in the sense that stacks
+$\bullet : \u F A \vdash S : \u B$ are bijective with values $x : A
+\vdash V : U \u B$, as both are bijective with computations $x : A
+\vdash M : \u B$.
 
 To compress the presentation in Figure~\ref{fig:gtt-syntax-and-terms},
 we use a typing judgement $\Gamma \mid \Delta \vdash M : \u B$ with a
@@ -1141,31 +1146,30 @@ empty or contains exactly one assumption $\bullet : \u B$, so $\Gamma
 : \u B \vdash M : \u B'$ is a stack.  The typing rules for $\top$ and
 $\with$ treat the stack input variable additively; for a function
 application to be a stack, the stack input must occur in the function
-position of a function application. 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
-input.
+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 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, \ldots, x_n : A_n \vdash e^* : \u F A$, where call-by-value
+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 \to \u F A')$.  Thus, a
-call-by-value term $e : A \to A'$, which should mean an effectful
+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 of type
-$e^* : \u F U (A \to \u F A')$. Here, the comonad $\u F U$ offers an
+$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,
 in addition to effects that are performed when the function is
 applied---so under transalation 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_n : \u B_n \vdash e : \u B$ is translated to $x_1 : U \u B_1, \ldots,
-x_n : U \u B_n \vdash e_* : \u B$, representing the fact that
-call-by-name terms are passed thunked arguments.  Product types are
+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 \to \u B'$ with a thunked argument.  Sums $B_1 +
-B_2$ are translated to $\u F (U \u B_1 + U \u B_2)$, making the
+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.
 
 %% While these rules are very intuitive when the input and output types
@@ -1204,21 +1208,23 @@ over either CBV or CBN for our purposes: it has enough judgements to
 express both kinds of extensionality rules.  For example, the
 extensionality principles for sums says that any complex value or
 computation $x : A_1 + A_2 \vdash E : T$ is equivalent to
-$\case{x}{x_1.E[\inl{x_1}/x]}{x_2.E[\inr{x_2}/x]}$, i.e. a case on a
-value can be moved around a program without changing its behavior.
-Given this, the above translations of CBV and CBN into CBPV explain why
-extensionality for sums holds in CBV but not CBN: in CBV, $x : A_1 + A_2
-\vdash E : T$ is translated to a term with $x : A_1 + A_2$ free, but in
-CBN, $x : B_1 + B_2 \vdash E : T$ is translated to a term with $x : U \u
-F(U \u B_1 + U \u B_2)$ free, and a monadic computation that returns a
-sum does not satisfy the $\eta$ principle for sums in CBPV.  Dually, the
-$\eta$ principle for functions in CBPV is that any computation $M : A
-\to \u B$ is equal to $\lambda x.M \, x$.  A CBN term $e : B \to B'$ is
-translated to a CBPV computation of type $U \u B \to \u B'$, to which
-CBPV function extensionality applies, while a CBV term $e : A \to A'$ is
-translated to a computation of type $\u F U(A \to \u F A')$, which does
-not satisfy the $\eta$ rule for functions.  We discuss a formal
-statement of these extensionality principles with term dynamism below.
+$\caseofXthenYelseZ{x}{x_1.E[\inl{x_1}/x]}{x_2.E[\inr{x_2}/x]}$, i.e. a
+case on a value can be moved to any point in a program (where all
+variables are in scope) in an optimization.  Given this, the above
+translations of CBV and CBN into CBPV explain why extensionality for
+sums holds in CBV but not CBN: in CBV, $x : A_1 + A_2 \vdash E : T$ is
+translated to a term with $x : A_1 + A_2$ free, but in CBN, $x : B_1 +
+B_2 \vdash E : T$ is translated to a term with $x : U \u F(U \u B_1 + U
+\u B_2)$ free, and the type $U \u F(U \u B_1 + U \u B_2)$ of monadic
+computations that return a sum does not satisfy the $\eta$ principle for
+sums in CBPV.  Dually, the $\eta$ principle for functions in CBPV is
+that any computation $M : A \to \u B$ is equal to $\lambda x.M \, x$.  A
+CBN term $e : B \to B'$ is translated to a CBPV computation of type $U
+\u B \to \u B'$, to which CBPV function extensionality applies, while a
+CBV term $e : A \to A'$ is translated to a computation of type $\u F U(A
+\to \u F A')$, which does not satisfy the $\eta$ rule for functions.  We
+discuss a formal statement of these extensionality principles with term
+dynamism below.
 
 %% \begin{mathpar}
 %%   \inferrule
@@ -1255,8 +1261,8 @@ add both $\dynv$ and $\dync$ to the grammar of types in
 Figure~\ref{fig:gtt-syntax-and-terms}.  We do \emph{not} give
 introduction and elimination rules for the dynamic types, because we
 would like constructions in GTT to imply results for many different
-possible implementations of the dynamic types.  Instead, the terms for
-the dynamic types will arise from type dynamism and casts.
+possible implementations of them.  Instead, the terms for the dynamic
+types will arise from type dynamism and casts.
 
 \subsection{Type Dynamism}
 
@@ -1278,13 +1284,12 @@ in the type dynamism ordering.  In \cite{fscd}, this last condition,
 \emph{the dynamic type is the most dynamic type}, then implies the
 existence of an upcast $\upcast{A}{\dynv}$ and a downcast
 $\dncast{A}{\dynv}$ which give a kind of intro and elim for the dynamic
-type: any type can be embedded into it and projected from it.  While
-this gives some information about the dynamic type, it by design does
-not characterize $\dynv$ uniquely up to isomorphism (e.g. as a recursive
-sum)---instead, it is left open-ended exactly which types exist, and
-therefore which injections/projections $\dynv$ has, to allow theorems in
-gradual type theory that are open-ended with respect to the addition of
-new types.
+type: any type can be embedded into it and projected from it.  By
+design, this does not characterize $\dynv$ uniquely up to isomorphism
+(e.g. as a recursive sum)---instead, it is left open-ended exactly which
+types exist, and therefore which injections/projections $\dynv$ has---so
+theorems in gradual type theory are open-ended with respect to the
+addition of new types.
 
 We extend this in a straightforward way to CBPV's distinction between
 value and computation types in Figure~\ref{fig:gtt-type-dynamism}: there
@@ -1359,9 +1364,9 @@ in the domain~\cite{fscd,icfp}.
 Even given previous work on call-by-value~\cite{icfp} and
 call-by-name~\cite{fscd} gradual typing, it is not immediately obvious
 how to add type casts to CPBV, because CBPV exposes finer judgemental
-distinctions than were considered in previous work.  However, we can use
-this previous work, with the embeddings of CBV and CBN into CBPV, for
-guidance.
+distinctions than previous work considered.  However, we can arrive at a
+first proposal by considering how previous work would be embedded into
+CBPV.
 %
 In the previous work on both CBV and CBN, every type dynamism judgement
 $A \ltdyn A'$ induces both an upcast from $A$ to $A'$ and a downcast
@@ -1376,11 +1381,12 @@ upcast and a downcast.
 In CBV, a cast from $A$ to $A'$ typically can be represented by a CBV
 function $A \to A'$, whose analogue in CBPV is $U(A \to \u F A')$, and
 values of this type are bijective with computations $x : A \vdash M : \u
-F A'$.  Since computations $x : A \vdash M : \u F A'$ are bijective with
-stacks $\bullet : \u F A \vdash \bindXtoYinZ{\bullet}{x}{M} : \u F A'$,
-this suggests that a \emph{value} type dynamism $A \ltdyn A'$ should
-induce an embedding-projection pair of \emph{stacks} $\bullet : \u F A
-\vdash S_u : \u F A'$ and $\bullet : \u F A' \vdash S_d : \u F A$.
+F A'$, and further with stacks $\bullet : \u F A \vdash
+\bindXtoYinZ{\bullet}{x}{M} : \u F A'$. This suggests that a
+\emph{value} type dynamism $A \ltdyn A'$ should induce an
+embedding-projection pair of \emph{stacks} $\bullet : \u F A \vdash S_u
+: \u F A'$ and $\bullet : \u F A' \vdash S_d : \u F A$, which allow both
+the upcast and downcast to a priori be effectful computations.
 %
 Dually, a CBN cast typically can be represented by a CBN function of
 type $B \to B'$, whose CBPV analogue is a computation of type $U \u B
@@ -1389,53 +1395,62 @@ Since computations $x : U \u B \vdash M : \u B'$ are bijective with
 values $x : U \u B \vdash \thunk{M} : U \u B'$, this suggests that a
 \emph{computation} type dynamism $\u B \ltdyn \u B'$ should induce an
 embedding-projection pair of \emph{values} $x : U \u B \vdash V_u : U \u
-B'$ and $x : U \u B' \vdash V_d : U \u B$.
+B'$ and $x : U \u B' \vdash V_d : U \u B$, where both the upcast and the
+downcast again may a priori be co-effectful, in the sense that they may
+not reflect all effects of their input.
 
 However, this analysis ignores an important property of CBV casts:
-upcasts always terminate without performing any effects, and in some
-systems upcasts are even defined to be values.  For example, an upcast
-from $A$ to $\dynv$ is often implemented as a sum/recursive type
-injection, which are value constructors.  In previous work on a logical
-relation for call-by-value gradual typing~\cite{icfp}, it was possible
-to prove that all upcasts had this property (but this depended on the
-only effects being divergence and type error).  In GTT, we can make this
-property explicit in the syntax of the casts, by making the upcast
-$\upcast{A}{A'}$ induced by a value type precision $A \ltdyn A'$ itself
-a complex value, rather than computation.  On the other hand, a downcast
-between value types is typically implemented as a case-analysis looking
-for a specific tag, and therefore can error, and so should be a
-computation, not a complex value.  
+\emph{upcasts} always terminate without performing any effects, and in
+some systems upcasts are even defined to be values, while only the
+\emph{downcasts} are effectful (introduce errors).  For example, an
+upcast from $A$ to $\dynv$ is often implemented as a sum/recursive type
+injection, which are value constructors.  Previous work on a logical
+relation for call-by-value gradual typing~\cite{icfp} proved that all
+upcasts had this property (but this depended on the only effects being
+divergence and type error).  In GTT, we can make this property explicit
+in the syntax of the casts, by making the upcast $\upcast{A}{A'}$
+induced by a value type precision $A \ltdyn A'$ itself a complex value,
+rather than computation.  On the other hand, a downcast between value
+types is typically implemented as a case-analysis looking for a specific
+tag, and therefore can error, and so should be a computation, not a
+complex value.
 
 In the present work, we make a dual observation about CBN casts.  The
 \emph{downcast} arising from $\u B \ltdyn \u B'$ has a stronger property
 than being a computation $x : U \u B' \vdash M : \u B$ as suggested
 above: it can be taken to be a stack $\bullet : \u B' \vdash \dncast{\u
-  B}{\u B'}{\bullet} : \u B$.  This formalizes the intuitive idea that a
-downcast evaluates the computation it is ``wrapping'' exactly once.
-Intuitively, this point of view is justified by thinking of the dynamic
-computation type $\dync$ as a recursive \emph{product} of all possible
-behaviors that a computation might have, and the downcast as a recursive
-type unrolling and product projection, which is a stack.  From this
-point of view, an \emph{upcast} can introduce errors, because the upcast
-of an object supporting some ``methods'' to one with all possible
-methods will error dynamically on the unimplemented ones.  
+  B}{\u B'}{\bullet} : \u B$---a downcast (behaves like it) evaluates
+the computation it is ``wrapping'' exactly once each type the downcasted
+computation is evaluated.  One intuitve justification for this point of
+view is to think of the dynamic computation type $\dync$ as a recursive
+\emph{product} of all possible behaviors that a computation might have,
+and the downcast as a recursive type unrolling and product projection,
+which is a stack.  From this point of view, an \emph{upcast} can
+introduce errors, because the upcast of an object supporting some
+``methods'' to one with all possible methods will error dynamically on
+the unimplemented ones.
 
 These observations are expressed in the (shaded) rules for casts in
 Figure~\ref{fig:gtt-syntax-and-terms}: the upcast for a value type
 precsion is a complex value, while the downcast for a computation type
-precsion is a stack (if its argument is).  Indeed, the description of
-the casts is simpler than the intuition we began the section with: from
-these two rules and monotonicity of type precsion for $U$/$\u F$ types,
-we automatically obtain the \emph{downcast} for a \emph{value} type
-precision $A \ltdyn A'$ as a stack $\bullet : \u F A' \vdash \dncast{\u
-  F A}{\u F A'}{\bullet} : \u F A$ as described above, representing the
-fact that the downcast might fail.  We also automatically obtain the
-upcast for a computation type precsion $\u B \ltdyn \u B'$ as a value $x
-: U \u B \vdash \upcast{U \u B}{U \u B'}{x} : U \u B'$ as suggested
-above.  Moreover, we will show below that the value upcast
-$\upcast{A}{A'}$ induces a stack $\bullet : \u F A \vdash \ldots : \u F
-A'$ that behaves like an upcast, and dually for the downcast, so this
-formulation is stronger than the one suggested above.
+precsion is a stack (if its argument is).  Indeed, this description of
+casts is simpler than the intuition we began the section with: rather
+than putting in both upcasts and downcasts for all value and computation
+types, it suffices to put in upcasts for value types and downcasts for
+computation types, because of monotonicity of of type dynamism for
+$U$/$\u F$ types.  For example, the \emph{downcast} for a \emph{value}
+type precision $A \ltdyn A'$, as a stack $\bullet : \u F A' \vdash
+\dncast{\u F A}{\u F A'}{\bullet} : \u F A$ as described above, is
+obtained from $\u F A \ltdyn \u F A'$ as computation types.  The upcast
+for a computation type precsion $\u B \ltdyn \u B'$ as a value $x : U \u
+B \vdash \upcast{U \u B}{U \u B'}{x} : U \u B'$ is obtained from $U \u B
+\ltdyn U \u B'$ as value types.  Moreover, we will show below that the
+value upcast $\upcast{A}{A'}$ induces a stack $\bullet : \u F A \vdash
+\ldots : \u F A'$ that behaves like an upcast, and dually for the
+downcast, so this formulation is stronger than the one suggested above,
+where both upcasts and downcasts for value types are stacks between $\u
+F$ types, and both downcasts and upcasts for computation types are
+values between $U$ types.
 
 We justify the stronger assertion that value type upcasts are complex
 values and computation type downcasts are complex stacks in two ways in
@@ -1445,7 +1460,7 @@ it is true, so there is at least one model where casts have these
 properties.  However, one goal of GTT is to be able to prove things
 about many gradually typed languages at once, by giving different
 interpretations of the syntax, so one might wonder whether this design
-rules out potential models where casts are only computations.  In
+rules out potential models where casts are effectful.  In
 Theorem~\ref{sec:thm:upcasts-values-downcasts-stacks}, we show instead
 that this design is forced for all casts, as long as the casts between
 ground types and the dynamic types have this property, which is true in