diff --git a/freyd-multicategories.tex b/freyd-multicategories.tex
index 1eae39ffca8011661db55c5ac282d5db8b953cdb..d92c499cb67a0c5eb9677178b01a07bf6690f889 100644
--- a/freyd-multicategories.tex
+++ b/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}