From 990d56cc21723ae244295a74854ae7e60cace504 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Fri, 19 Jan 2024 14:36:38 -0500
Subject: [PATCH] describe Kleisli action on squares
---
paper-new/appendix.tex | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/paper-new/appendix.tex b/paper-new/appendix.tex
index 0106135..4914837 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
--
GitLab