Oh, this is annoying, because it seems to mean that we would need unbounded search (to drop all "hcom []"'s) until we can read the |x,a|, which is against the spirit of, say, Martin-Loef type theories. Martin
On Thursday, 7 March 2019 22:51:20 UTC, dlicata wrote:
That would be true if the term you are normalizing is in the empty interval context, and the cubical type theory has “empty system regularity” (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf).
Otherwise, if you evaluate something in the empty interval context, you might see something like
hcom [] (hcom [] (hcom [] (hcom [] (… |x,a| … ))))
with |x,a| in there somewhere. In HITs, Kan composition is treated as a constructor of the type, and though there are no interesting lines to compose in the empty interval context, the uninteresting compositions don’t vanish in all flavors of cubical type theory.
> On Mar 7, 2019, at 5:41 PM, Martín Hötzel Escardó <escardo...@gmail.com> wrote:
>
> So I presume that when we ask cubical Agda to normalize a term of type || Sigma (x:X), A x || we will get a term of the form |x,a| and so we will see the x in normal form, where |-| is the map into the truncation, right? Martin.
>
> On Thursday, 7 March 2019 21:52:12 UTC, Anders Mörtberg wrote:
> 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.