diff --git a/paper-new/appendix.tex b/paper-new/appendix.tex
index 01061357ebba5806dde2f95b6c211b431b142448..4914837eb4f4bd7771b712f81cdddbfd4691b793 100644
--- a/paper-new/appendix.tex
+++ b/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