* 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 tight morphisms are the (p □ q), i.e (p □ id) o (id □ q) or the equivalent flipped version. 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. ** ... wrt Funny Cartesian Product of M-Cats We want a monad T that freely constructs an M-cat such that 1. (TC)_tight is a cartesian category 2. TC is a monoid with respect to the □-monoidal structure on M-cat. So we define (TC)t to be the free cartesian category on Ct. TC_l is generated by 1. For every p ∈ (TC)t, a morphism (ret p) ∈ (TC)l 2. For every A₁,...,Aᵢ,...,Aₙ and morphism p : Ai -> B, a morphism \[ let i = p \] 3. Satisfying hm... ** Freyd Multicategories as T-multicategories 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 ret : C1ᵥ(Γ;A) -> C1ₜ(Γ;A) - For every object A, a pure identity arrow id(A) : C1ᵥ(A;A) - For every let-sequence T(C1ₜ)ₜ(Δ1,...,Δn ; Γ) and term C1ₜ(Γ;A), a term C1ₜ(Δ1,...,Δn;A) - 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