We are going to show that in MLTT with propositional truncation the type
$$\textstyle
\prod_{A:U_0}\prod_{B:U_0}
(\|A\| \to A) \times (\|B\| \to B) \to (\|A + B\| \to A + B)
$$
has no inhabitants. Assume it did.
We shall work in a specific model of MLTT with propositional truncation, namely assemblies over number realizability. It is not too important what this model is precisely, except for the following facts:
- there is an object of reals $\mathbb{R}$ in which
- $\Pi (x : \mathbb{R}) \; \|(x < 1) + (x > 0)\|$, and
- every map $\mathbb{R} \to \mathsf{bool}$ is constant.
Hoever, using the above type, we may inhabit
$$\Pi(x : \mathbb{R}) \; \|x < 1\| + \|x > 0\|,$$
contradicting the fact that every map $\mathbb{R} \to \mathsf{bool}$ is constant.
To do so, consider any $x : \mathbb{R}$ and instantiate $A = \|x < 1\|$ and $B = \|x > 1\|$ (and use the fact that $<$ maps into propositions).
\|A\|
to give you $\|A\|$ instead of $||A||$. $\endgroup$