From ff7da08e9d788f5fd1fccf3feff490ad87e94ab2 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 28 Mar 2018 11:09:12 -0400
Subject: [PATCH] [sketch] start spelling out freyd multicategory

---
 sketch.org | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

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