freyd-multicategories.tex

\documentclass{article}

\usepackage{amsmath,amssymb}
\usepackage{tikz-cd}
\usepackage{mathpartir}

\newtheorem{theorem}{Theorem}
\newtheorem{definition}{Definition}

\newcommand{\Set}{\text{Set}}
\newcommand{\relto}{\to}
\newcommand{\M}{\mathcal{M}}
\newcommand{\sq}{\square}
\newcommand{\lett}{\text{let}\,\,}

\begin{document}
\title{Freyd Multicategories as Generalized Multicategories}
\author{Max S. New}
\maketitle
\begin{abstract}
  Based on work of Power, we present the \emph{Freyd Multicategories}
  of Staton-Levy as a form of Generalized Multicategories (Leinster,
  Crutwell-Shulman) relative to the monad whose algebras are strict
  Freyd categories. Following Crutwell-Shulman, we could also call
  these \emph{Virtual Freyd Categories}. We plan for this to be the
  basis for our call-by-value gradual type theory, by adapting the
  construction from Set to Poset/Cat.
\end{abstract}

\section{M-categories and Freyd Categories}

First, we recount and re-organize some details of Power on freyd
categories as $\M$-categories with algebraic structure.

\begin{definition}[Sierpinski, Mono]
  Define $\to$ to be the free category with two objects and one arrow
  between them.  Then the Sierpinski topos is the category
  $\Set^{\to}$ of arrows and commuting squares is a preasheaf topos
  and the category Mono of injective functions and
  commuting squares is a quasitopos: the category of
  $\neg\neg$-separated presheaves on $\Set^{\to}$.
\end{definition}

We can then form the double categories of Sierpinski and
Mono-matrices, the right place to define categories enriched in
Sierpinski and Mono.

\begin{definition}[Mat($V$)]
  The virtual equipment of Sierpinski (Mono) matrices has as vertical
  category the category of sets and functions and a horizontal arrow
  $M : X \relto Y$ is a matrix giving for each $(x,y)\in X\times Y$ an
  object of Sierpinski (Mono).  A globular 2-cell is given by an arrow
  in Sierpinski (Mono) for each $x,y$ and the restriction of matrix $M
  : X \relto Y$ by functions $f : X' \to X$ and $g : Y' \to Y$ is
  given by $((f,g)^*M)_{x',y'} = M_{f(x'),g(y')}$.
  
\end{definition}

\begin{definition}[Sierpinski Categories]
  The virtual equipment of sierpinski categories and functors/profs is
  given by Mod(Mat(Sierp))
  
  More explicitly, a Sierpinski category $C$ consist of a set of
  objects $C_0$, a category structure of ``tight'' morphisms $C_t$ and
  a category of ``loose'' morphisms $C_l$ with an injective function
  $i : C_t(a,b) \to C_l(a,b)$ that preserves identity and composition.
\end{definition}

Next, we consider ordered and cartesian Freyd Categories as
(Sierp)/Mono-categories with ``algebraic structure'', we give a more
pedestrian presentation than Power.

First, planar freyd categories are monoidal sierpinski-categories
using the following ``funny'' tensor product, which we can define on
the double category of matrices, and thus automatically for
categories.
%
The idea is that the funny tensor product is the cartesian product of
the tight maps and blah
\begin{definition}[Funny Tensor Product of Matrices]
  We define a ``funny tensor product'' $\sq$ on the double category of
  Sierpinksi matrices by setting the action on vertical categories to
  be the cartesian product, and on matrices:
  \begin{enumerate}
  \item $(C \sq D)_0 = C \times D$
  \item $(C \sq D)_{x,y,t} = C_{x,y,t} \times D_{x,y,t}$
  \item $(C \sq D)_{x,y,l}$ is the following \emph{pushout}:
    \[
\begin{tikzcd}
C_t\times D_t = (C\sq D)_t \arrow[d] \arrow[r] & C_t \times D_l \arrow[d] \\
C_l \times D_t \arrow[r] & (C \sq D)_l
\end{tikzcd}
\]
  I.e, it is the quotient of the sum $(C_l \times D_t) + (C_t \times
  D_l)$ by the equivalence induced by $(i_C(f_l),g_l) = (f_l,
  i_D(g_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
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
\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.
%
Further, we will likely (for the models' sake) need to develop
``double'' freyd multicategories as well.
%

I've had several false starts here.
%
Here's 2 options that are \emph{close}, but no cigar.

First, in analogy with double categories, we could just take
categories internal to Mono-categories, so a span of mono-categories
with identity and unit.
%
However, a span of Mono-categories is not quite right.
%
You have an object mono-category, representing objects and vertical
morphisms, but then your arrows are also a mono-category, so you have
only a \emph{set} of arrows, and tight and loose \emph{squares} and
source and target take tight squares to tight vertical morphisms.
%
So this is definitely not right

Second, instead of looking at $\Set^{\to}$ and its refinement to Mono,
we could start with $\text{Preorder}^{\to}$ or $\text{Cat}^{\to}$ and
refine those somehow.
%
I think something here \emph{includes} our categories, but is also too
big. Need to look into this more.

%% To get that, we can use categories \emph{internal} to Mono-categories.

%% \begin{definition}[Double Mono-Category]
%%   A double Mono Category is a category internal to the category of
%%   Mono categories.

%%   I \emph{conjecture} that it is equivalent to a double category of
%%   ``loose'' vertical and horizontal arrows, and a sub-double-category
%%   with the same objects.
%% \end{definition}

%% To get a preordered Mono category, there are two places to modify the
%% definition: at Mono, or at category internal to.
%% %
%% To get the right double category structure for the multicategory
%% stuff, this is the right order:

%% \begin{definition}[Threeorder/3-Valued Preorder/Inclusion of Preorders]
%%   A 3-valued Preorder or inclusion of preorders is a category enriched
%%   in the ordinal 3: $0 \leq 1 \leq 2$, which is a reflective
%%   subcategory of $\text{Set}^{\to}$ defined by taking a set $X$ to the
%%   truth value $\exists x\in X. \top$.

%%   They are equivalent to an object with a ``tight'' and ``loose''
%%   ordering, where tight ordering implies loose ordering.
%% \end{definition}

%% \begin{definition}[Threeorder Category/Wide Double Subcategory]
%%   A threeorder category is a category internal to threeorders.

%%   It is equivalent (I think) to a pair of preorder category structures
%%   on the same set of objects, where the preorder structures form a
%%   threeorder, and the category structures form a Mono category.
%% \end{definition}

\subsection{Kleisli Construction}

Basically, take Coreflection(Kl(C,T))

\end{document}

%% Local Variables:
%% compile-command: "pdflatex freyd-multicategories.tex"
%% End: