diff --git a/paper/gtt.tex b/paper/gtt.tex
index ab62b39e9e197167fe782d354edf7747dbfaac94..4278ebad90f44378dbdd833e51844967a5bde7a2 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1576,15 +1576,18 @@ relevant definitions and facts:
     $A$ and $A'$}, which consists of two complex values $x : A \vdash V'
     : A'$ and $x' : A' \vdash V : A$ such that $x : A \vdash V[V'/x']
     \equidyn x : A$ and $x' : A' \vdash V'[V/x] \equidyn x' : A'$.
-  \item We write $\u B \cong_v \u B'$ for a \emph{computation
+  \item We write $\u B \cong_c \u B'$ for a \emph{computation
     isomorphism between $\u B$ and $\u B'$}, which consists of two
-    complex stacls $\bullet : \u B \vdash S' : \u B'$ and $\bullet' : \u
+    complex stacks $\bullet : \u B \vdash S' : \u B'$ and $\bullet' : \u
     B' \vdash S : \u B$ such that $\bullet : \u B \vdash S[S'/x']
     \equidyn \bullet : \u B$ and $\bullet' : \u B' \vdash S'[S/\bullet]
     \equidyn \bullet' : \u B'$.
   \end{enumerate}
 \end{definition}
 
+FIXME: Note that an effectful isomorphism is a computation isomorphism
+between $\u F$ types and dually~\cite{levy16popl}.  
+
 \smallskip
 
 \begin{lemma}[Intitial objects] ~ \label{lem:initial}
@@ -2281,8 +2284,8 @@ Dually, we have
 \end{proof}
 
 
-\begin{theorem}{Functorial Casts} \label{thm:functorial-casts}
-  \begin{small}
+\begin{theorem}{Cast Unique Implementation Theorem for $+,\times,\to,\with$} \label{thm:functorial-casts}
+\begin{small}
 \[
   \begin{array}{l}
     \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})}}\\
@@ -2917,7 +2920,7 @@ it seems that we cannot prove that $x : \leastdynv \vdash
 
 \begin{theorem}[Least Dynamic Computation Type]
 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 \leastdynv
+B$, and we have a terminal computation type $\top$, then $U \leastdync
 \cong_{v} U \top$.
 \end{theorem}
 \begin{proof}
@@ -2925,7 +2928,7 @@ 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,
 because $\top$ is not a strict terminal object, the dual of the above
-argument does not give a stack isomorphism $\leastdynv \cong_c \top$.
+argument does not give a stack isomorphism $\leastdync \cong_c \top$.
 
 However, using the retract axiom, we have
 \[
@@ -3038,7 +3041,7 @@ define their universal property:
 \[
   {x : A' \vdash \defdncast{A}{A'}{x} \ltdyn x : A \ltdyn A'}
   \qquad
-  {x \ltdyn x' : A \ltdyn A' \vdash x \ltdyn \dncast{A}{A'} x' : A}
+  {x \ltdyn x' : A \ltdyn A' \vdash x \ltdyn \defdncast{A}{A'} x' : A}
 \]
 \end{definition}
 
@@ -3049,8 +3052,9 @@ upcasts/downcasts, the analogues of these theorems hold for computation
 upcasts and value downcasts as well.
 
 Some value downcasts and computation upcasts do exist, leading to a
-characterization of the casts for the monad/comonad of $F \dashv U$:
-\begin{theorem}[Monadic/Comonadic Casts] \label{thm:monadic-comonadic-casts}
+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}
   Suppose $A \ltdyn A'$ and $\u B \ltdyn \u B'$.  
   \begin{enumerate}
   \item $\bullet : \u F A \vdash
@@ -3372,7 +3376,7 @@ universal property already existing).
 
 \subsection{Equidynamic Types are Isomorphic}
 
-\begin{theorem}
+\begin{theorem}[Equidynamism implies Isomorphism] 
   \begin{enumerate}
   \item
     If $A \ltdyn A'$ and $A' \ltdyn A$ then $A \cong_v A'$.