diff --git a/.gitignore b/.gitignore index 3e52f7bac2606862224f00ed8d7b332dddea8eae..fc4c644c092df19e29b0f06e0bc181f05b48324b 100644 --- a/.gitignore +++ b/.gitignore @@ -219,3 +219,4 @@ TSWLatexianTemp* # expex forward references with \gathertags *-tags.tex *.agdai +*.pdf diff --git a/freyd-multicategories.tex b/freyd-multicategories.tex new file mode 100644 index 0000000000000000000000000000000000000000..a341e284cc4fa4598473400d179f7f46626115fe --- /dev/null +++ b/freyd-multicategories.tex @@ -0,0 +1,113 @@ +\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}