Re: [HoTT] Propositional Truncation

[Ben Sherman <sherman@csail.mit.edu>]

[-- Attachment #1: Type: text/plain, Size: 5249 bytes --]

On a similar note, I had originally (and mistakenly, at least according to the terminology in the HoTT book, which I looked up) thought that declaring “A is inhabited” rather than just “A” was meant to refer to the type || A || rather than A, in which case, I read the question “if || A || is inhabited, then A is inhabited” as

|| || A || || -> || A ||

The above statement does hold, and in some way I think of this (though I’m not sure how to connect it formally) as an internalization of Dan’s and Martin’s external statements.

(According to the HoTT book, we say “A is merely inhabited” to say || A ||.)

> On Mar 7, 2019, at 11:16 AM, Martín Hötzel Escardó <escardo.martin@gmail.com> wrote:
> 
> I got confused now. :-)
> 
> Seriously now, what you say seems related to the fact that from a proof |- t : || X || in the empty context, you get |- x : X in cubical type theory. This follows from Simon's canonicity result (at least for X=natural numbers), and is like the so-called "existence property" in the internal language of the free elementary topos. This says that from a proof |- exists (x:X), A x in the empty context, you get |- x : X and |- A x. This says that exists in the empty context behaves like Sigma. But only in the empty context, because otherwise it behaves like "local existence" as in Kripke-Joyal semantics. 
> 
> Martin
> 
> On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote:
> Just in case anyone reading this thread later is confused about a more beginner point than the ones Nicolai and Martin made, one possible stumbling block here is that, if someone means “is inhabited” in an external sense (there is a closed term of that type), then the answer is yes (at least in some models): if ||A|| is inhabited then A is inhabited.  For example, in cubical models with canonicity, it is true that a closed term of type ||A|| evaluates to a value that has as a subterm a closed term of type A (the other values of ||A|| are some “formal compositions” of values of ||A||, but there has to be an |a| in there at the base case).  This is consistent with what Martin and Nicolai said because “if A is inhabited then B is inhabited” (in this external sense) doesn’t necessarily mean there is a map A -> B internally.   
> 
> -Dan 
> 
> > On Mar 5, 2019, at 6:07 PM, Martín Hötzel Escardó <escardo...@gmail.com <>> wrote: 
> > 
> > Or you can read the paper https://lmcs.episciences.org/3217/ <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 <>. 
> >> For more options, visit https://groups.google.com/d/optout <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 <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 <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <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.

[-- Attachment #2: Type: text/html, Size: 7441 bytes --]