On Friday, 8 March 2019 15:13:14 UTC, dlicata wrote:
nice! the negation trick is clever.
Yes, this is really nice.
Martin, I don’t understand why this situation is any different than natural numbers, though. If I have a closed term of type nat, I can normalize it, but then I (externally) need to read through all of the successors to figure out what number it is. (Or maybe I can only weak head normalize it, in which case I need to interleave further weak head normalization after every successor.) Is this an unbounded search? The parallel is to read “hcom []” as successor and “|x,a|” as zero.
Except that you would have different normal forms for the same thing, and this thing would be prefixed by an unbounded number of *printed* clock ticks.
It is not right to say that unbounded search is needed, I agree. But it wouldn't be pleasant to have to see 10^6 ticks. I would rather wait for 10^6 units of time (which should be fast) and then see the answer than see a million hcomp's followed by the answer on my computer screen . :-)
Fortunately, Anders says that the clock ticks are not printed in the version of cubical type theory implemented by Agda --cubical, which is nice!
Martin
-Dan
> On Mar 8, 2019, at 9:59 AM, Anders Mortberg <andersm...@gmail.com> wrote:
>
> In fact, in Cubical Agda you will not get these hcomp's with empty
> systems. The reason is that because of the way hcomp works in Agda
> there is a very nice trick to implement the "generalized hcomp"
> operation of the paper that Dan linked to. I summarized the trick in:
>
> https://github.com/agda/agda/issues/3415
>
> I added this to Agda some month ago and it should be possible to
> update Simon's canonicity proof to get a stronger result saying that
> the only elements of HITs in the empty context are point constructors
> (like in the AFH paper). For this to work you also have to impose a
> "validity" constraint (Def 12 in the ccctt paper Dan linked to) so
> that empty systems cannot result from substitutions. This is currently
> not done in Cubical Agda, but if you start with a term with only valid
> systems then you should never get an empty system.
>
> So the extraction of witnesses from existence statements should work
> as Martín said in Cubical Agda.
>
> --
> Anders
>
> On Thu, Mar 7, 2019 at 6:23 PM Martín Hötzel Escardó
> <escardo...@gmail.com> wrote:
>>
>> And this is a wildly speculative question. If we used Andrew Swan's identity type derived from the cubical path type only, as in the abstract library file https://github.com/agda/cubical/blob/master/Cubical/Core/HoTT-UF.agda) would we still get this phenomenon? Maybe not? What I mean is that we use normal Agda, together with what is offered in that file and nothing else (so that we are using HoTT book axiomatic type theory). Martin
>>
>> On Thursday, 7 March 2019 23:01:33 UTC, Martín Hötzel Escardó wrote:
>>>
>>> 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.
>>>>
>> --
>> 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.