diff --git a/sketch.org b/sketch.org index c8d7ab9219c13f49533b46397eea9afc8644e9fc..79e767d212ce2665db6e6469b56e5f373837c210 100644 --- a/sketch.org +++ b/sketch.org @@ -28,6 +28,20 @@ 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