Skip to content
Snippets Groups Projects
Commit ff7da08e authored by Max New's avatar Max New
Browse files

[sketch] start spelling out freyd multicategory

parent 71db74fa
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment