Choose term of coproduct type We work in homotopy type theory. Denote the propositional truncation of a type $A$ by $\|A\|$ and the function type between types $A$ and $B$ by $A \to B$.
Can you construct a term of the following type:
$$
\prod_{A:U_0}\prod_{B:U_0} 
(\|A\| \to A) \times (\|B\| \to B) \to (\|A + B\| \to A + B)
\quad?
$$
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 &lt; 1) + (x &gt; 0)\|$, and
every map $\mathbb{R} \to \mathsf{bool}$ is constant.

Hoever, using the above type, we may inhabit
$$\Pi(x : \mathbb{R}) \; \|x &lt; 1\| + \|x &gt; 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 &lt; 1\|$ and $B = \|x &gt; 1\|$ (and use the fact that $&lt;$ maps into propositions).