From 71db74fa3766460e87f1279905d3246eefc4fef0 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Tue, 6 Mar 2018 11:20:57 -0500
Subject: [PATCH] definition of freyd multicategory (with specified central
 morphisms)

---
 sketch.org | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 sketch.org

diff --git a/sketch.org b/sketch.org
new file mode 100644
index 0000000..c8d7ab9
--- /dev/null
+++ b/sketch.org
@@ -0,0 +1,34 @@
+* Freyd Multicategories as Generalized Multicategories
+
+(Based on Discussion with Mike Shulman about Premonoidal Categories)
+
+First, there is a double category of Subset Matrices whose objects are
+sets, vertical arrows are functions, horizontal arrows $R : A -/-> B$
+are for each a,b a set $R_l(a,b)$ with a specified subset $R_t(a,b)
+\subset R_l(a,b)$. A monoid in this double category is an M-category
+or a pure-effectful category which has a set of objects, for each pair
+of objects a set of "loose arrows" which are "possibly effectful", a
+subset of "tight arrows" which are "pure" such that any composable
+string of tight arrows is tight (including empty string, i.e. the
+identity).
+
+There is a "funny cartesian" monoidal product called â–¡ and defined by
+generators and relations as follows. $C â–¡ D$ has as objects pairs
+(c,d) of objects. Arrows are generated by for each arrow $f : c -> c'$
+and object d in D, there is an arrow $f â–¡ id$ and vice-versa for
+arrows in D. Subject to the following equations:
+    (f â–¡ id) o (f' â–¡ id) = (f o f' â–¡ id)
+    (id â–¡ g) o (id â–¡ g') = (id â–¡ g o g')
+    (p â–¡ id) o (id â–¡ g) = (id â–¡ g) o (p â–¡ id)
+    (id â–¡ q) o (f â–¡ id) = (f â–¡ id) o (id â–¡ q)
+where p,q are tight morphisms.
+The monoids with respect to â–¡ are strict premonoidal categories with a
+specified subset of the central morphisms.
+Restricted to tight arrows, it is the cartesian produt.
+
+There should be a free monoid monad T on M-category, and then "freyd
+multicategories" should be T-multicategories.
+
+These have a set C0 of objects, for every list of objects G and object
+A a set of loose morphisms C_l(G;A) with a specified subset of tight
+morphisms
-- 
GitLab