Truncation and $\Pi$-types (ii) I just read Ximei's post Truncation and $\Pi$-types. Can anyone explain in simple terms why ($\star$) implies ($\star\star$) but not vice versa. In other words, I wonder why ($\star$) is stronger than ($\star\star$).
$$||\prod_{x:A}B(x)||\quad(\star)\quad\quad\quad\quad\prod_{x:A}||B(x)||\quad(\star\star)$$
Thanks!
 A: This fact actually corresponds in a very natural way with a classical fact of (Zermelo-Fraenkel) set theory: namely, that the axiom of choice is equivalent to the statement that a Cartesian product of any family of non-empty sets is itself non-empty. Now, in homotopy type theory, for any type $C$, the type $||C||$ should be thought of as containing precisely the information of whether $C$ is inhabited, and nothing more. In other words, there is a canonical map $C\to||C||$ that collapses all of the internal structure of $C$ except whether $C$ inhabited. If we read "inhabited" as "non-empty", then the statement $(\star)$ can be thought of as expressing that $\prod_{x:A}B(x)$ is non-empty, while the statement $(\star\star)$ can be thought of as expressing that $B(x)$ is non-empty for every $x:A$.
This gives us a very natural "classical" analogue of $(\star)$ in Zermelo-Fraenkel set theory, which we will denote $(\bullet)$; this is the assertion that a Cartesian product of family of sets $(B_x)_{x\in A}$, indexed by a set $A$, is non-empty. Similarly, the "classical" analogue of $(\star\star)$, which we will denoted $(\bullet\bullet)$, is the assertion that $B_x$ is non-empty for every $x\in A$. In ZF set theory, $(\bullet)$ always implies $(\bullet\bullet)$, since the Cartesian product of any family of sets that includes the empty set is itself empty. However, as stated above, the assertion that $(\bullet\bullet)$ implies $(\bullet)$ in general is equivalent to the axiom of choice. As you can see, this gives a very precise analogue of the situation with $(\star)$ and $(\star\star)$ in homotopy type theory. With this in mind, let me fill in the details of the proof given in the question you linked to; hopefully this will clarify what's going on.

Recall that, for any $x:A$, the type $||B(x)||$ is a mere proposition, meaning that we have $a=b$ for any $a,b:||B(x)||$. We claim also that the dependent product of a family of mere propositions is itself a mere proposition, whence $\prod_{x:A}||B(x)||$ is a mere proposition as well. To see this, note that, for any $f,g:\prod_{x:A}||B(x)||$, showing $f=g$ amounts by function extensionality to showing $f(x)=g(x)$ for any $x:A$. But each $f(x),g(x):||B(x)||$, and hence, since $||B(x)||$ is a mere proposition, we have $f(x)=g(x)$ for each $x:A$, as desired.
Now, the type $||\prod_{x:A}B(x)||$ has the following constructor: for any element $f:\prod_{x:A}B(x)$, there is an element $|f|:||\prod_{x:A}B(x)||$. This constructor allows us to formulate the recursion principle of $||\prod_{x:A}B(x)||$:

If $C$ is any mere proposition and $\alpha:\left(\prod_{x:A}B(x)\right)\to C$, then there is an induced element $\overline{\alpha}:||\prod_{x:A}B(x)||\to C$ satisfying $\overline{\alpha}(|f|)\equiv \alpha(f)$ for any $f:\prod_{x:A}B(x)$.

In particular, since $\prod_{x:A}||B(x)||$ is a mere proposition, to define a element of type $$||\prod_{x:A}B(x)||\to\prod_{x:A}||B(x)||,$$ it suffices to define an element of type $\prod_{x:A}B(x)\to\prod_{x:A}||B(x)||$. We claim that such an element is given by the expression $\lambda f.\lambda x.|f(x)|$, where $|\cdot|$ is the constructor for $||B(x)||$. Indeed, if $f$ is of type $\prod_{x:A}B(x)$, then $f(x)$ is of type $B(x)$ for any $x:A$, and so we have $|f(x)|:||B(x)||$ for each $x:A$, as desired.
On the other hand, there is no such way of constructing an element of type $$\prod_{x:A}||B(x)||\to||\prod_{x:A}B(x)||,$$ without some additional axioms. The reason for this is that, a priori, there is no way of "lifting" an element of $||B(x)||$ to an element of $B(x)$. In particular, if we wanted to construct an element of $||\prod_{x:A}B(x)||$, we would first need to construct an element of $\prod_{x:A}B(x)$; if we only have an element $f:\prod_{x:A}||B(x)||$ on hand, then we're able to get elements of $||B(x)||$ from elements $x:A$, but there's no way to to get elements of $B(x)$ from those elements of $||B(x)||$, and so we're stuck.
