One can make the following type algebraic transformation (where $=$ means isomorphic and $\equiv$ means syntactically equal): $$ X * (X \to X) \;\; \equiv \;\; X * X^X = \\ X^{(1+X)} \;\; \equiv \;\; (1+X) \to X $$
Is there an analogous transformation starting with the following dependent type: $$ P 0 * (\forall n, P n \to P (S n)) \;\; \equiv \;\; ??? $$
(For definiteness, I’ll use Martin-Löf type theory, with the notation of $\sum$ and $\prod$ for dependent sums/products, so my $\prod$ is your $\forall$. If you had a substantially different system or interpretation of the $\forall$ in mind, then my apologies for misunderstanding.)
The following seems a fairly analogous transformation: $$ \textstyle \newcommand{\N}{\mathbb{N}} P(0) \times (\prod_{n : \N} P(n) \to P(Sn)) \cong \prod_{z : \left(1 + \sum_{n:\N}P(n)\right)} P(\text{case $z$ of $\operatorname{inl}(x)\mapsto 0,\, \operatorname{inr}(y) \mapsto S(\pi_1(y))$}).$$
This follows from the distributivity properties between dependent function types and binary sums / dependent sums $$\textstyle \prod_{x:A} (B(x) \to C(x)) \cong \prod_{y : \sum_{x:A} \! B(x)} C(\pi_1(y)) \qquad \qquad A \cong \prod_{x:1} A $$ $$ \textstyle \prod_{x:A} C(x) \times \prod_{y:B} D(y) \cong \prod_{z : A + B} \left(\text{case $z$ of $\operatorname{inl}(x)\mapsto C(x),\, \operatorname{inr}(y) \mapsto D(y)$}\right)$$ which are the dependent versions of the properties involved in your original isomorphism.