From 23292a06dda5265982df0bc07f2bea0155e0ced1 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 25 Jan 2024 14:42:22 -0500
Subject: [PATCH] fix build issues, progress on CBPV semantics
---
paper-new/appendix.tex | 36 ++++++++++++++++++++++++++++++++++++
paper-new/intro.tex | 2 +-
2 files changed, 37 insertions(+), 1 deletion(-)
diff --git a/paper-new/appendix.tex b/paper-new/appendix.tex
index 9c179c7..9cb558e 100644
--- a/paper-new/appendix.tex
+++ b/paper-new/appendix.tex
@@ -111,6 +111,42 @@ precision:
\section{Call-by-push-value}
+\subsection{Morphisms of CBPV Models}
+
+There are two relevant notions of \emph{morphism} of CBPV models:
+\emph{strict} and \emph{lax}.
+% morphisms of CBPV models
+Given call-by-push-value models
+$\mathcal M_1 = (\mathcal V_1, \mathcal E_1, \arr_1, U_1, F_1)$ and
+$\mathcal M_2 = (\mathcal V_2, \mathcal E_2, \arr_2, U_2, F_2)$,
+A \emph{strict} morphism $G$ from $M_1$ to $M_2$ is given by a pair of functors
+$G_{\mathcal{V}}: V_1 \to V_2$ and $G_{\mathcal{E}} : E_1 \to E_2$
+that strictly presere the constructors:
+\begin{enumerate}
+ \item $G_{\mathcal{E}} \circ F_1 = F_2 \circ G_{\mathcal{V}}$
+ \item $G_{\mathcal{V}} \circ U_1 = U_2 \circ G_{\mathcal{E}}$
+ \item $G_{\mathcal{E}}(A \arr_1 B) = G_{\mathcal{V}}(A) \arr_2 G_{\mathcal{E}}(B)$
+ \item $G_{\mathcal{V}}(A_1 \times_1 A_2) = G_{\mathcal{V}}(A_1) \times_2 G_{\mathcal{V}}(A_2)$
+ \item $G_{\mathcal{V}}(1_1) = 1_2$
+\end{enumerate}
+As well as strictly preserving the corresponding universal morphisms
+and coherence isomorphisms.
+
+A lax morphism instead preserves these only up to transformation
+\begin{enumerate}
+ \item $G_{\mathcal{E}} \circ F_1 \Rightarrow F_2 \circ G_{\mathcal{V}}$
+ \item $G_{\mathcal{V}} \circ U_1 \Rightarrow U_2 \circ G_{\mathcal{E}}$
+ \item $G_{\mathcal{E}}(A \arr_1 B) \Rightarrow G_{\mathcal{V}}(A) \arr_2 G_{\mathcal{E}}(B)$
+ \item $G_{\mathcal{V}}(A_1 \times_1 A_2) \Rightarrow G_{\mathcal{V}}(A_1) \times_2 G_{\mathcal{V}}(A_2)$
+ \item $G_{\mathcal{V}}(1_1) \Rightarrow 1_2$
+\end{enumerate}
+Additionally a lax morphism should have a relationship between these
+transformations and the universal morphisms, but we will only consider
+lax morphisms of thin categories, where such conditions hold
+trivially.
+
+\subsection{Kleisli Actions of CBPV Type Constructors}
+
In CBPV models, all the type constructors are interpreted as functors:
\begin{enumerate}
\item $\to : \op\calV \times \calE \to \calE$
diff --git a/paper-new/intro.tex b/paper-new/intro.tex
index 3d6a3bc..d822b4a 100644
--- a/paper-new/intro.tex
+++ b/paper-new/intro.tex
@@ -155,7 +155,7 @@ exhibit the categorical construction. New and Licata
\cite{new-licata18} present such a model using categories of
$\omega$-CPOs, and this model was extended by Lennon-Bertrand,
Maillard, Tabareau and Tanter to prove graduality of a gradual
-dependently typed calculus $\textrm{CastCIC}^{\mathcalG}$. This
+dependently typed calculus $\textrm{CastCIC}^{\mathcal G}$. This
domain-theoretic approach meets our criteria of being a semantic
framework for proving graduality, but suffers from the limitations of
classical domain theory: the inability to model viciously
--
GitLab