Construct function from a truncated proposition In the remark below Cor 3.9.2 in HoTT book it says to construct a function from $ ||A|| $ to $ B $, we define a predicate $ Q:B\to\mathcal{U} $ such that $ \Sigma_{x:B}Q(x) $ is a mere proposition. Then we construct an $ f:A\to\Sigma_{x:B}Q(x) $, gets a $ g:||A||\to\Sigma_{x:B}Q(x) $ by the recursion principle of propositional truncation and finally projects it to $ B $. But how can $ \Sigma_{x:B}Q(x) $ be a mere proposition if $ B $ is not? Because this means all elements in $ \Sigma_{x:B}Q(x) $ are equal, which indicates their first component must be equal. Is it supposed to be viewed as a "subtype" of $ B $ here? Also what's the connection here with Cor 3.9.2? 
The books says an example of this method is Exercise 3.19:

Suppose $ P:\mathbb{N}\to\mathcal{U} $ is adecidable family of mere propositions. Prove that
  $$ \Vert\Sigma_{n:\mathbb{N}}P(n)\Vert\to\Sigma_{n:\mathbb{N}}P(n). $$

My attempt is below: $ P $ is decidable means every $ P(n)$ satisefies LEM, thus either $ P(n)\simeq\mathbf{1} $ or $ P(n)\simeq\mathbf{0} $. In the simple case when $ 
P(0)\simeq\mathbf{1} $, consider the type family $ \Sigma_{n:\mathbb{N}}(0=n)\times P(n) $, I guess this would be contractible and in paticular mere propositoin. So the constant map $ (n,p_{n})\mapsto(0,\mathsf{refl}_{0},p_{0}) $ factors through $ \Vert\Sigma_{n:\mathbb{N}}P(n)\Vert $. Am I correct? Also, this requires some $ P(n_{0})\simeq\mathsf{1} $, but generally we can't guarantee this. How about the general case? Would anyone help me? Thanks in advance!
 A: Just because all elements of $\sum_{x:B} Q(x)$ are equal doesn't mean all elements of $B$ are equal, because there may be no way to select for every $x:B$ an element of $Q(x)$ to lift it to an element of $\sum_{x:B} Q(x)$.
It's true that if there exists a function $f:\prod_{x:B} Q(x)$ and $\sum_{x:B} Q(x)$ is a proposition, then so is $B$, since for any $x,y:B$ we have $(x,f(x)):\sum_{x:B} Q(x)$ and $(y,f(y)):\sum_{x:B} Q(x)$, hence $(x,f(x))=(y,f(y))$ and so $x=y$.  This is just another way of saying that propositions are closed under retracts, since giving $f$ is exhibiting $B$ as a retract of $\sum_{x:B} Q(x)$.
As a simple example of how this can fail, fix some $b:B$ and let $Q(x) :\equiv (b=x)$.  Then $\sum_{x:B} Q(x)$ is a based path-space, hence contractible and thus in particular a proposition.  But $B$ could have been any pointed type.
I agree that the connection with 3.9.2 is not immediately clear.  I think probably the idea was to take $A$ and $P$ in the lemma to be $\Vert A \Vert$ and the constant family at $\sum_{x:B} Q(x)$, respectively.  Then the desired function $\Vert A\Vert \to \sum_{x:B} Q(x)$ can be obtained from the lemma by observing that $\sum_{x:B} Q(x)$ is a proposition (by assumption) and that our function $A\to \sum_{x:B} Q(x)$ yields $\Vert A \Vert \to \Vert \sum_{x:B} Q(x)\Vert$.
A: For Exercise 3.19, you can use that if $P$ holds for some number, there is a smallest number for which $P$ holds. This can be proven by an algorithm which scans down from the given number. The following type is a mere proposition because of the uniqueness of the smallest number:
$$\Sigma_{n:\mathbb{N}}P(n)\times({\textstyle\prod}_{m} P(m)\to n\leq m)$$
Hence you can eliminate into it from $\Vert\Sigma_{n:\mathbb{N}}P(n)\Vert$, then project out the first two components.
