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

| cite | improve this answer | |
  • $\begingroup$ 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! $\endgroup$ – Greywhite Apr 5 at 8:55
  • $\begingroup$ 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. $\endgroup$ – Mike Shulman Apr 6 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.

| cite | improve this answer | |
  • $\begingroup$ 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? $\endgroup$ – Greywhite Apr 6 at 14:28
  • $\begingroup$ "Eliminator" is another name for the recursion/induction rules. $\endgroup$ – Mike Shulman Apr 6 at 15:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.