# 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!

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$$.

• Thanks for answering! I think maybe the connection with Cor 3.9.2 is that they both follow from Lem 3.9.1? Also I edited the question. Looking foward to some advice on Ex 3.19.Thanks! Apr 5 '20 at 8:55
• The book specifically says that the corollary encapsulates a technique of reasoning, so I think it's talking about more than just following from the same lemma. Apr 6 '20 at 15:43

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.

• I don't quite understand what is the eliminator of truncation, i.e. how do we use it. The book talks about constructor, recursion and induction rules, just not eliminator. I know there is no universal function $\Vert A\Vert\to A$, then how do we write the "inhabitedness" of $A$ formally? Apr 6 '20 at 14:28
• "Eliminator" is another name for the recursion/induction rules. Apr 6 '20 at 15:42