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 as a partially applied bifunctor $C\colon\ \mathsf{Set}/\mathcal{P}(A)\times\mathsf{Set}/\mathcal{P}(A)\to \mathsf{Set}/\mathcal{P}(A)$, partially applied to $(A,\lambda x.\,\{x\})$.

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.

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.

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 as a partially applied bifunctor $C\colon\ \mathsf{Set}/\mathcal{P}(A)×\mathsf{Set}/\mathcal{P}(A)→ \mathsf{Set}/\mathcal{P}(A)$, partially applied to $(A,λx.\,\{x\})$.

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

My List base functor would then be $L_0(R,r) := (1,λ\_.\,\emptyset ) + C_0\left(\left(A,λ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 $μ$ (join) of the Action Monad (aka Writer monad), but can't quite put my finger on it.

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 as a partially applied bifunctor $C\colon\ \mathsf{Set}/\mathcal{P}(A)\times\mathsf{Set}/\mathcal{P}(A)\to \mathsf{Set}/\mathcal{P}(A)$, partially applied to $(A,\lambda x.\,\{x\})$.

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.