You can't have a function which, for all A, gives you ||A|| -> A. See the exercises 3.11 and 3.12! -- Nicolai On 05/03/19 22:31, Jean Joseph wrote: > 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. -- 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.