Equivalence between lax algebras for parametrised endofunctors and iterated monads

Let $(\cM,\times,1)$ be a cartesian monoidal category, let $(\cC,\blacktriangleright)$ be an $\cM$-actegory, and let $F$ be a strong endofunctor on $\cC$ such that $F$ and $\cC$ satisfy the hypotheses of the stated Kelly theorem. For a lax algebra $(X,(P,f))$ for $\mathsf{Para}(F)$, let $P$ carry the comonoid structure

$$!_P:P\to 1,\qquad \Delta_P:P\to P\times P.$$

Equivalence conjecture. The assignment sending $(X,(P,f))$ to the corresponding lax algebra for $F^\kappa$,

$$(X,(P,f))\longmapsto (X,((P,!_P,\Delta_P),\underrightarrow{\mathsf{laxlim}}((P,f)\circ\mathsf{Para}(F)(P,f)\circ\cdots\circ\mathsf{Para}(F)^\alpha(P,f)):F^\kappa X\to X)),$$

defines an equivalence of categories

$$\mathsf{Lax}\textbf{-}\mathsf{Alg}_{\mathsf{Endo}}(\mathsf{Para}(F))\longrightarrow \mathsf{Lax}\textbf{-}\mathsf{Alg}_{\mathsf{Mnd}}(F^\kappa).$$

The claim identifies lax algebras for parametrised endofunctors with lax algebras for the associated iterated monad, using the induced comonoid of parameters. Its resolution depends on the hypotheses invoked from the Kelly theorem and the construction of the displayed lax limit; the supplied text gives no status evidence beyond the statement itself.