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 $\mathbf{M}$ whose underlying span is
$S \stackrel{dom}{\leftarrow} M \stackrel{cod}{\to} 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^\ast \to S$ where the domain is the free monoid on $S$. Now, the free cartesian monoidal category $\mathbf{C}$ on (the discrete category) $S$ has as its objects elements of $S^\ast$, and so its underlying span will look like
$S^\ast \stackrel{src}{\leftarrow} C \stackrel{tar}{\to} S^\ast,$and now I think the underlying span of the free cartesian monoidal category on the monoidal category $\mathbf{M}$ is the span composite of
$S \leftarrow S^\ast \stackrel{src}{\leftarrow} C \stackrel{tar}{\to} S^\ast \to S$followed by $S \stackrel{dom}{\leftarrow} M \stackrel{cod}{\to} S$. Abusing notation, let $\mathbf{M} \circ \mathbf{C}$ denote this span composite.
The distributive law will be a morphism of spans of the form $\mathbf{C} \circ \mathbf{M} \to \mathbf{M} \circ \mathbf{C}$. I’ll only give an example for how this goes. Suppose $m: s \to t$ is a morphism in $\mathbf{M}$, and let $\delta_t: t \to t \otimes t$ be the copy morphism. Then $m; \delta_t$ is formally rewritten as $\delta_s; (m \otimes m)$. Hopefully this makes the general idea clear.
1 to 9 of 9