From 7199e9f634f867be9989c8b3eff091cb015a4836 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 28 Mar 2018 17:53:49 -0400
Subject: [PATCH] sketch is looking very sketchy at this point :/

---
 sketch.org | 27 ++++++++++++++++++++++-----
 1 file changed, 22 insertions(+), 5 deletions(-)

diff --git a/sketch.org b/sketch.org
index 79e767d..a991b3f 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
-- 
GitLab