squeeze some space

paper-new/categorical-model.tex

@@ -43,15 +43,14 @@ In summary, an extensional model consists of:
 \begin{enumerate}
   \item A locally thin reflexive graph internal to CBPV models.
   \item Composition of value and computation relations that form a category with the reflexive relations as identity. Call these categories $\mathcal V_r,\mathcal E_r$
-  \item An identity-on-objects functor $\upf : \mathcal V_r \to \mathcal V_f$ taking each value relation to a morphism that universally left-represents it.
-  \item An identity-on-objects functor $\dnf : \mathcal E_r^{op} \to \mathcal E_f$ taking each computation relation to a morphism that universally right-represents it.
-  \item The CBPV connectives $U,F,\times,\to$ are all \emph{covariant} functorial on relations up to equivalence\footnote{the reflexive graph structure already requires that these functors preserve identity relations}
-    \begin{itemize}
-    \item $U(dd') \equidyn U(d)U(d')$
-    \item $F(cc') \equidyn F(c)F(c')$
-    \item $(cc') \to (dd') \equidyn (c \to d)(c' \to d')$
-    \item $(c_1c_1') \times (c_2c_2') \equidyn (c_1 \times c_2)(c_1'\times c_2')$
-    \end{itemize}
+  \item Identity-on-objects functors $\upf : \mathcal V_r \to \mathcal V_f$ and $\dnf : \mathcal E_r^{op} \to \mathcal E_f$ such that every $\upf c$ universally left-represents $c$ and every $\dnf d$ universally represents $d$.
+  \item The CBPV connectives $U,F,\times,\to$ are all \emph{covariant} functorial on relations up to equivalence: $U(dd') \equidyn U(d)U(d')$ etc.\footnote{the reflexive graph structure already requires that these functors preserve identity relations}
+    %% \begin{itemize}
+    %% \item $U(dd') \equidyn U(d)U(d')$
+    %% \item $F(cc') \equidyn F(c)F(c')$
+    %% \item $(cc') \to (dd') \equidyn (c \to d)(c' \to d')$
+    %% \item $(c_1c_1') \times (c_2c_2') \equidyn (c_1 \times c_2)(c_1'\times c_2')$
+    %% \end{itemize}
     where $c \equidyn c'$ means $\id \ltsq{c}{c'}\id$ and $\id \ltsq{c'}{c} \id$.
   \item A natural transformation $\mho : 1 \Rightarrow U$ such that
     $\mho \circ ! \ltsq{r(A)}{r(UB)} f$ for any $f : A \to UB$
@@ -70,8 +69,8 @@ gradual typing in Section~\ref{sec:GTLC}.
   \item Each type $A$ as a value type, interpreting the base types and
     $\times$ as their semantic analogues and $\sem {A \ra A'}$ as $U(\sem{A} \to
     F(\sem{A'}))$.
-  \item Every type precision derivation $c : A \ltdyn A'$ is
-    interpreted as a relation morphism $\sem{c} : \sem{A} \rel \sem{A'}$ in the obvious
+  \item Type precision derivations $c : A \ltdyn A'$ are
+    interpreted as relation morphisms $\sem{c} : \sem{A} \rel \sem{A'}$ in the obvious
     way. Every equivalence axiom $c \equiv c'$ implies that $\sem{c} \equidyn \sem{c'}$.
   \item Every term $\Gamma \vdash M : A$ is interpreted as a morphism
     $\sem{M} : \mathcal V_f (\times\sem{\Gamma},UF\sem{A})$. Upcasts are interpreted as