start definition of freyd categories as generalized multicategories

.gitignore

@@ -219,3 +219,4 @@ TSWLatexianTemp*
 # expex forward references with \gathertags
 *-tags.tex
 *.agdai
+*.pdf

freyd-multicategories.tex

+\documentclass{article}
+
+\usepackage{amsmath,amssymb}
+\usepackage{tikz-cd}
+
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{definition}{Definition}
+
+\newcommand{\Set}{\text{Set}}
+\newcommand{\relto}{\to}
+\newcommand{\M}{\mathcal{M}}
+\newcommand{\sq}{\square}
+
+\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?
+\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 tight
+morphisms is a cartesian product. I don't know how to describe this in
+terms of adjoints.
+
+\end{document}