The existence property is proved for CCHM cubicaltt by Simon in:
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.