describe Kleisli action on squares

paper-new/appendix.tex

@@ -62,6 +62,12 @@ example for the function type is functorial in each argument:
 \item $A \tok \id = \id$
 \end{enumerate}
 
+Finally, note that all of these constructions lift to squares in a
+double CBPV model since the squares themselves form a CBPV model and
+the projection functions preserve CBPV structure. For instance, given a square
+$\alpha : l \ltdyn_{F c_o}^{F c_i} l'$ and a horizontal morphism $d : B \rel B'$ of appropriate type, we get a square
+\[ \alpha \tok d : l \tok B \ltdyn_{U(c_o \to d)}^{U(c_i \to d)} l' \tok B' \]
+
 \section{Details of the Construction of an Extensional Model}
 
 In Section \ref{sec:extensional-model-construction}, we outline the construction