define free freyd category, conjecture about preorder version

freyd-multicategories.tex

@@ -2,7 +2,7 @@
 
 \usepackage{amsmath,amssymb}
 \usepackage{tikz-cd}
-
+\usepackage{mathpartir}
 
 \newtheorem{theorem}{Theorem}
 \newtheorem{definition}{Definition}
@@ -11,6 +11,7 @@
 \newcommand{\relto}{\to}
 \newcommand{\M}{\mathcal{M}}
 \newcommand{\sq}{\square}
+\newcommand{\lett}{\text{let}\,\,}
 
 \begin{document}
 \title{Freyd Multicategories as Generalized Multicategories}
@@ -96,19 +97,139 @@ C_l \times D_t \arrow[r] & (C \sq D)_l
   \end{enumerate}
   I checked on the board that it maps 2-cells, and it must be
   functorial, right?
+
+  The unit of the funny tensor product is the terminal object: $1 \to
+  1$.
 \end{definition}
 
 By abstract nonsense, the funny tensor product on the equipment of
 matrices becomes a monoidal product on the equipment of categories,
-and then a planar premonoidal category is a monoid object wrt the
-funny tensor product. In more pedestrian terms, a planar premonoidal
+and then a (planar) premonoidal category is a monoid object wrt the
+funny tensor product. In more pedestrian terms, a (planar) premonoidal
 category has a monoidal category of tight morphisms, a premonoidal
 category of loose morphisms and all tight morphisms are central.
 
 A freyd category is then a \emph{cartesian} premonoidal category:
-i.e. a premonoidal category where the monoidal structure on the tight
-morphisms is a cartesian product. I don't know how to describe this in
-terms of adjoints.
+i.e. a premonoidal category where the monoidal structure on the
+\emph{tight} morphisms is a cartesian product. I don't know how to
+describe this as an adjoint or something in the category of sierpinski
+categories, but you can just use the functor to ordinary categories
+that takes the tight category and say the monoidal structure is
+cartesian.
+
+\subsection{(Strict) Freyd Categories are Monadic}
+
+Next, we show that Freyd categories can be presented as algebras of a
+monad.
+%
+This is also true of planar and symmetric premonoidal categories, but
+we focus on the cartesian case here.
+
+\begin{definition}[Free Strict Freyd Category]
+  We define the free strict Freyd category $TC$ of a Sierpinski
+  category $C$ as follows.
+  \begin{enumerate}
+  \item The objects are lists of objects of $C$: $(TC)_0 = C_0^*$.
+  \item The tight morphisms are given by the free cartesian category,
+    i.e. they are \emph{substitutions}:
+    \[
+    TC(a_1,\ldots,a_n;b_1,\ldots,b_m)_t = \sum_{\rho : [m] \to [n]}\prod_{0 < i \leq m} C(a_{\rho i},b_i)
+    \]
+  \item The loose morphisms are defined inductively as follows.
+    \begin{enumerate}
+    \item First we have the inclusion of tight morphisms: for every
+      substitution $\gamma : TC(\Gamma,\Delta)_t$ there is a loose
+      morphism $i(\gamma) : TC(\Gamma,\Delta)_l$.
+    \item Next, we need to include the loose generators, so for every
+      $f : C(a,a')_t$, we have a rule
+      \begin{mathpar}
+        \inferrule
+        {f : C_t(a_i,b)\and
+          p : TC(a_1,\ldots,a_n;\Gamma)
+        }
+        {\lett n+1 = f(i); p : TC(a_1,\ldots,a_n,b;\Gamma)}
+      \end{mathpar}
+    \item Next, we define composition in two steps. First, we define
+      composition of a loose morphism with a tight morphism by
+      induction on the (output) loose morphism. Then we define
+      composition of loose morphisms by induction on the input
+      morphism.
+      \begin{mathpar}
+        \begin{array}{rcl}
+          (\lett n+1 = f(i);p) \circ (\rho, \gamma : TC(\Gamma, a_1,\ldots,a_n)) & = &
+          \lett |\Gamma|+1 = (f \circ \gamma(i))(\rho(i)); (p \circ (\rho,\gamma)[|\Gamma|+1/|\Gamma|+1])\\
+
+          (\rho,\gamma) \circ (\rho',\gamma') & = & \cdots
+        \end{array}
+
+        \begin{array}{rcl}
+          (\lett n+1 = f(i);p);q &=& \lett n+1 = f(i); (p;q)\\
+          (\rho,\gamma);q &=& q \circ (\rho,\gamma)
+        \end{array}
+      \end{mathpar}
+    \item First, there are two ways to include a tight generator: in a
+      substitution and using the inclusion of loose generators, so we
+      add an axiom that those are equal:
+      \[
+      (\lett 2 = i(v)(1); (1,2)) \cong (1,v(1))
+      \]
+      which we can write in a more reduction rule style:
+      \[
+      (\lett n+1 = i(v)(j); p) \cong p \circ v(j)/n+1
+      \]
+    \item Finally, to ensure functoriality of the inclusion of loose
+      generators, we add in a functoriality axiom.
+      \[
+      (\lett 2 = f(1); \lett 3 = g(2); (3)) \cong (\lett 2 = (g \circ f)(1); (2))
+      \]
+    \end{enumerate}
+  \end{enumerate}
+\end{definition}
+
+I claim that that's a monad, its strict algebras are strict freyd
+categories and its pseudo-algebras are freyd categories.
+
+\section{Freyd Multicategories from the Free Freyd Category Monad}
+
+A Freyd Multicategory is then a normalized T-monoid, following
+Crutwell-Shulman.
+%
+Instead, we will use \emph{discrete} T-monoids, those whose underlying
+object category is a set, though I don't think the theorem in
+Crutwell-Shulman here applies.
+
+\begin{definition}[Freyd Multicategory]
+  A Freyd Multicategory $M$ consists of
+  \begin{enumerate}
+  \item A set of objects $M_0$
+  \item For every object $A \in M_0$ and list of objects $\Gamma \in
+    M_0^*$, a set of tight morphisms $M(\Gamma;A)_t$ and loose
+    morphisms $M(\Gamma;A)_l$.
+  \item Tight composition
+  \item Loose composition
+  \end{enumerate}
+\end{definition}
+
+
+\subsection{Free Freyd Multicategory}
+
+\section{Preordered Freyd Categories and Multicategories}
+
+Now we want to combine Freyd (multi)categories with preordered
+categories to get preorderd Freyd (multi)categories.
+%
+The difficulty is that preordered categories are a type of
+\emph{internal} category, but Freyd categories are a type of
+\emph{enriched} category.
+
+Thinking heuristically, we probably want our version of a Mono
+preorder category to be equivalent to a full embedding of preorder
+categories: there are types, a preorder category modeling effectful
+terms and ordinary type precision, and a wide (and tall?)
+sub-double-category of pure terms and pure type precision.
+
+Conjecture: a Mono preorder category is a preorder internal to Mono
+categories.
 
 \end{document}