Or you can read the paper https://lmcs.episciences.org/3217/ regarding what 
Nicolai said.

Moreover, in the HoTT book, it is shown that if || X||->X holds for all X, 
then univalence can't hold. (It is global choice, which can't be invariant 
under equivalence.)

The above paper shows that unrestricted ||X||->X it gives excluded middle. 

However, for a lot of kinds of types one can show that ||X||->X does hold. 
For example, if they have a constant endo-function. Moreover, for any type 
X, the availability of ||X||->X is logically equivalent to the availability 
of a constant map X->X (before we know whether X has a point or not, in 
which case the availability of a constant endo-map is trivial).

Martin

On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote:
>
> 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 <javascript:>.
> 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.