Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Added a link to Todd’s nice page on free cartesian category.
(Only seeing this now.)
That sounds right, mattecapu. But I think a nice way of viewing it is by using distributive laws between spans. The rough idea is that morphisms in the free cartesian category can be presented in a “standard” form, as a “purely cartesian morphism” c (a morphism in the free cartesian monoidal category on the underlying set of objects) followed by a morphism m in the monoidal category. I’ll denote this by c|m. When it comes time to compose two such morphisms, say c|m followed by d|n, you rewrite m;d into a new form d′;m′ by using naturality of copy and delete, and then the composite will be c;d|m′;n. The distributive law is this rewriting process.
Slightly more formally, I think it goes like this. Suppose given a monoidal category M whose underlying span is
Sdom←Mcod→S.I think technically it might be easier dealing with strict monoidal categories here, so I’ll just assume that for now. By strictness, the monoidal structure on the object level gives a map S*→S where the domain is the free monoid on S. Now, the free cartesian monoidal category C on (the discrete category) S has as its objects elements of S*, and so its underlying span will look like
S*src←Ctar→S*,and now I think the underlying span of the free cartesian monoidal category on the monoidal category M is the span composite of
S←S*src←Ctar→S*→Sfollowed by Sdom←Mcod→S. Abusing notation, let M∘C denote this span composite.
The distributive law will be a morphism of spans of the form C∘M→M∘C. I’ll only give an example for how this goes. Suppose m:s→t is a morphism in M, and let δt:t→t⊗t be the copy morphism. Then m;δt is formally rewritten as δs;(m⊗m). Hopefully this makes the general idea clear.
1 to 9 of 9