Re: [HoTT] Propositional Truncation

["Anders Mörtberg" <andersmortberg@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 4736 bytes --]

The existence property is proved for CCHM cubicaltt by Simon in:

https://arxiv.org/abs/1607.04156

See corollary 5.2. This works a bit more generally than what Martín said, 
in particular in any context with only dimension variables we can compute a 
witness to an existence. So if in context G = i_1 : II, ..., i_n : II  
(possibly empty)  we have:

G |- t : exists (x : X), A(x)

then we can compute G |- u : X so that G |- B(u).

--
Anders

On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, Martín Hötzel Escardó 
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/ 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. 
>> > 
>> > 
>> > -- 
>> > 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.

[-- Attachment #1.2: Type: text/html, Size: 6480 bytes --]