Is this kind of functor $\mathsf{Set}/M×\mathsf{Set}/M\to \mathsf{Set}/M$, with $M$ a monoid, a known construction?

Question

I'm trying to construct lists with elements of type $A$ as the initial algebra over a base endofunctor in $\mathsf{Set}/\mathcal{P}(A)$, such that the list is indexed by the set of its elements.

My idea is to model Cons using a bifunctor $C\colon\ \mathsf{Set}/\mathcal{P}(A)\times\mathsf{Set}/\mathcal{P}(A)\to \mathsf{Set}/\mathcal{P}(A)$.

My definition of $C$ would be $C_0 (X,f) (Y,g) := (X\times Y, \lambda(a,b).\,f(a)\cup g(b))$.

My List base functor would then be $L_0(R,r) := (1,\lambda\_.\,\emptyset ) + C_0\left(\left(A,\lambda x.\,\{x\}\right),\left(R,r\right)\right)$.

My question is: Is this kind of bifunctor $C$ a known construction? I find what it does reminiscent of the $\mu$ (join) of the Action Monad (aka Writer monad), but can't quite put my finger on it.

Answer 1

In general, for any monoidal category $(\mathcal M, \otimes, I)$ and a monoid $(m, *, i) \in \mathcal M$, the slice category $\mathcal M/m$ inherits the monoidal structure pointwise, i.e. the tensor product is given by taking morphisms $f : x \to m$ and $g : y \to m$ to the morphism $x \otimes y \xrightarrow{f \otimes g} m \otimes m \xrightarrow{*} m$, and the unit is given by $i : I \to m$.

In your example, we take $(\mathbf{Set}, \times, 1)$ to be the category of sets equipped with cartesian monoidal structure and $(m, *, i)$ to be the power set monoid $(\mathcal P A, \cup, \varnothing)$.

Abstractly, we can see resulting tensor product on $\mathbf{Set}/\mathcal{P}A$ to be given by the following composite

$$(\mathbf{Set}/\mathcal{P}A)^2 \simeq (\mathbf{Set}^{\mathcal{P}A})^2 \xrightarrow{\langle-,-\rangle} (\mathbf{Set}^2)^{({\mathcal{P}A}^2)} \xrightarrow{\times^{({\mathcal{P}A}^2)}} \mathbf{Set}^{({\mathcal{P}A}^2)} \simeq \mathbf{Set}/({\mathcal{P}A}^2) \xrightarrow{\mathbf{Set}/\cup} \mathbf{Set}/{\mathcal{P}A}$$

where the equivalences are given by the correspondence between indexed sets and $\mathbf{Set}$-functors from discrete categories.

The unit is given similarly by

$$1 \xrightarrow{1} \mathbf{Set} \simeq \mathbf{Set}/1 \xrightarrow{\mathbf{Set}/i} \mathbf{Set}/{\mathcal{P}A}$$