Disjoint union types in MLTT

Question

In MLTT, by identifying propositions as types (and vice versa), a proposition carries the information regarding how a proof of the proposition is constructed. My question is related to this. Let $P:\textsf{U}$, then by definition, $(*)$ and $(**)$ are both well-formed types: $$P+\neg P\quad(*)\quad\quad\quad\Pi X:\{P,\neg P\}.X+\neg X\quad (**)$$ In traditional logic, $(*)$ is equivalent to LEM; whilst $(**)$ expresses that for every $X$ that belongs to the set $\{P,\neg P\}$, LEM holds for $X$. In traditional logic, $(*)$ and $(**)$ are trivially equivalent to each other. My question is, given the proof-relevant property of propositions in MLTT, are $(*)$ and $(**)$ still mutually derivable? Thanks!