* 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.
What does this free monoid look like?

Let's spell this structure out and then see how to simplify.
A freyd multicategory consists of

1. An underlying M-category of "unary" pure and effectful morphisms
   C0.
2. A T-module of multi-arrows, i.e. a module C1 : T(C0) <-/- C0. This
   consists of
   - For every list Γ ∈ C0* and output type A ∈ C0, a set of pure
     morphisms C1ᵥ(Γ;A) and effectful morphisms C1ₜ(Γ;A) and an
     injective function i : C1ᵥ(Γ;A) -> C1ₜ(Γ;A)
   - For every object A, a pure identity arrow id(A) : C1ᵥ(A;A)
   - TODO: the rest

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