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ó > 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. > > -- 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.