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](https://ncatlab.org/nlab/show/action+monad) (aka Writer monad), but can't quite put my finger on it.



Is this kind of functor $\mathsf{Set}/M×\mathsf{Set}/M\to \mathsf{Set}/M$, with $M$ a monoid, a known construction?
In general, for any monoidal category $(\mathcal M, \otimes, I)$ and a monoid $(m, \*, i) \in \mathcal M$, the [slice category](https://ncatlab.org/nlab/show/over+category#examples) $\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](https://ncatlab.org/nlab/show/cartesian+monoidal+category) 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}$$


