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? 

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.