diff --git a/sketch.org b/sketch.org index 79e767d212ce2665db6e6469b56e5f373837c210..a991b3fb9ae57f56fe50f056033e2e68e240455a 100644 --- a/sketch.org +++ b/sketch.org @@ -22,13 +22,28 @@ arrows in D. Subject to the following equations: (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. -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? +** ... 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 @@ -39,9 +54,11 @@ A freyd multicategory consists of 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) + injective function ret : C1áµ¥(Γ;A) -> C1â‚œ(Γ;A) - For every object A, a pure identity arrow id(A) : C1áµ¥(A;A) - - TODO: the rest + - 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