Hi,
From the HoTT book, the truncation of any type A has two constructors:
1) for any a : A, there is |a| : ||A||
2) for any x,y : ||A||, x = y.
I get that if A is inhabited, then ||A|| is inhabited by (1). But is it true that, if ||A|| is inhabited, then A is inhabited?