I'm trying to formalize some of my code within Category Theory, and I ended up having to prove that a certain construction $(T,\lambda,\rho)$ was a monad. Here is the setup. Let $(D,\eta,\mu)$ be a monad over $\mathbf{Set}$. Now,I want to define a monad $(T,\lambda, \rho)$ over the slice category $\mathbf{Set}/D P$.
The construction is the following, $T(A,f) = (DA, \mu Df)$ for objects. A morphism $\phi \in \text{Hom}_{\mathbf{Set}/D P}((A,f),(B,g))$ is a function $\phi:A \to B$ such that the commutation $g\circ \phi = f$ is true. Thus, we define $Tf = Df$.
If I'm not mistaken, $T:\mathbf{Set}/DP \to \mathbf{Set}/DP$ is a functor, which can be seen from the fact that $T(f\circ g) = D(f\circ g) = Df \circ Dg = Tf \circ Tg$, which follows from the fact that $D$ is a functor. The same idea applies to the identity morphism.
Now we must define $\lambda$ and $\rho$. The idea is again just to make them equal to the $\eta$ and $\mu$ counterparts. For every object $(A,f) \in \mathbf{Set}/DP$ we have $$ \lambda_{(A,f)}:(A,f)\to (DA,\mu Df) \ \text{ where } \ \lambda_{(A,f)}=\eta_A $$ $$ \rho_{(A,f)}:(A,f)\to (DA,\mu Df) \ \text{ where } \ \rho_{(A,f)}=\mu_A $$
The monadic properties would be inherited from $(D,\eta, \mu)$. This would prove that $(T,\lambda,\rho)$ is a monad in $\mathbf{Set}/DP$. Is this proof correct?