From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33e.google.com (mail-ot1-x33e.google.com [IPv6:2607:f8b0:4864:20::33e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1a7c06a8 for ; Fri, 8 Mar 2019 22:29:00 +0000 (UTC) Received: by mail-ot1-x33e.google.com with SMTP id k15sf9567122otn.18 for ; Fri, 08 Mar 2019 14:29:00 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=OL8KjsZfi5EJi13aSC/nedzl99PyFC26UakEY/5uY7E=; b=qnMWBVK3jAiTtGj5oyr4kpYqAF1GU103/MeBjmh8EKln78BtvUrIBKJZenn/w0FMoE WjMgizlhk/3jeOwksm2S196YHxlRAaLMdL8aEhQCqX0ghV3OlHxxpEPngZhfPck3X/YJ /w9sv1r14xLXsLXuC+/uJ+nvYVUNkjW36Gi1bUDZjv3qlyqG4pKj94dh7K6GnoFxU5x2 A/LCdmNiyesgzbHPyll/HwIgZnMkV8HdPtuenStJF4WvYiNwCXEmmEXhk89jAr/wH/su sAxGk6+7A/48R1bWIpFmZaxS8VqZfyP3APf1xK57kyaIiydlr52OGbECPwAuwlZZwjv6 CMyA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=OL8KjsZfi5EJi13aSC/nedzl99PyFC26UakEY/5uY7E=; b=SQAbGCojG/RhteNCr0HiCsFWLX5irkHS5ayKb3DZTad7KBpMOCy4AaSvZgmsOKd4i0 felml2SfXGyYzKkwv3fX1Z98/hg+yaQIDQgLDmeTw17bb4rTuZ3Aaexjbi1FK+61rqfy u7fLcjGHxw7cdYgXdKhkXWlmpeuh2prJud/amDTX7F8YxonOcTrQwXc1WU2HTH6eSJvV broWLR2RHqX/8JYjJ0wr6mm3TQABnZxyUvlu+3vQ3QSP79GIy++gFddyDUaw6heQ94oA P6aLSmbyD18yDRAkM36FwQztDZfI6ti/+s0IeWazwpidE29hgF2UEEysUnfBM7iHdclJ PpFw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=OL8KjsZfi5EJi13aSC/nedzl99PyFC26UakEY/5uY7E=; b=YNlYS1mNY2MPHB35g6+EAq0EbPBKmb5hNKx2HW2b/Hy3uoYumMZZPY49lhRkS+KgHm b44qz3g/I3u9EkLZ9g5wC8Ky3dCSW6PvPHWoll8DeYCKN4wVAt1WCel7P5p1WMZp7V3L UtoOVY1piZHVP6c0sRvnAP6skgUEQvFVMhzujNhoTBxRDTi4cKC0zNH5IKcY9GUXBJGP NSmHCo0hh57pHpGSA04SGkdchG6xkdfRZZoxhDZR3oyq3sZgvyukSkkdu/DQjhadQHTm d3FOjGpt8+9sEz2a5ifBgEN4Ls1hIcEz1R9iT3pQPWznDznYsF4LBhCDV5tECUjBL88Y rf6Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXTnCCdpgQ2O/6ZewJXKe6ZyhD/chO3PNRPAdJaG+dv898lD5/2 FpFJPte/ubX3qMrA+r9a+oY= X-Google-Smtp-Source: APXvYqw5XiVPbksJMKnnOq9U9gv7/JmAWAiPO1vKpg5OsQ1CLHniXHbnK31Bd+msgVAMrUL77/lspw== X-Received: by 2002:a05:6830:15c7:: with SMTP id j7mr12361002otr.331.1552084139805; Fri, 08 Mar 2019 14:28:59 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:c4c1:: with SMTP id u184ls2707012oif.8.gmail; Fri, 08 Mar 2019 14:28:59 -0800 (PST) X-Received: by 2002:aca:4542:: with SMTP id s63mr10227721oia.106.1552084138934; Fri, 08 Mar 2019 14:28:58 -0800 (PST) Date: Fri, 8 Mar 2019 14:28:58 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: In-Reply-To: References: <0f5b8d0e-9f1d-47a7-9d39-a9112afb77ea@googlegroups.com> <12cd6b73-7ca6-481c-9503-250af28b8113@googlegroups.com> <30ae0dc4-cef2-46ad-a280-bdf617a0db4e@googlegroups.com> <9fbd1c51-139e-4657-980a-2264a8f9ff92@googlegroups.com> <5f7932a1-417b-42be-9d63-300dddc83037@googlegroups.com> <98CB1099-377A-4A5F-94F2-B33C36D577B0@wesleyan.edu> <50111384-09a4-4c30-8272-fa9e5997d3c3@googlegroups.com> <7a7c3e3f-df35-42ea-9d89-f0d20b855e9e@googlegroups.com> Subject: Re: [HoTT] Propositional Truncation MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1409_1448670496.1552084138225" X-Original-Sender: escardo.martin@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_1409_1448670496.1552084138225 Content-Type: multipart/alternative; boundary="----=_Part_1410_162976777.1552084138226" ------=_Part_1410_162976777.1552084138226 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Friday, 8 March 2019 15:13:14 UTC, dlicata wrote: > > nice! the negation trick is clever.=20 > Yes, this is really nice. Martin, I don=E2=80=99t understand why this situation is any different than= natural=20 > numbers, though. If I have a closed term of type nat, I can normalize it= ,=20 > but then I (externally) need to read through all of the successors to=20 > figure out what number it is. (Or maybe I can only weak head normalize i= t,=20 > in which case I need to interleave further weak head normalization after= =20 > every successor.) Is this an unbounded search? The parallel is to read= =20 > =E2=80=9Chcom []=E2=80=9D as successor and =E2=80=9C|x,a|=E2=80=9D as zer= o. =20 > > Except that you would have different normal forms for the same thing, and= =20 this thing would be prefixed by an unbounded number of *printed* clock=20 ticks.=20 It is not right to say that unbounded search is needed, I agree. But it=20 wouldn't be pleasant to have to see 10^6 ticks. I would rather wait for=20 10^6 units of time (which should be fast) and then see the answer than see = =20 a million hcomp's followed by the answer on my computer screen . :-) Fortunately, Anders says that the clock ticks are not printed in the=20 version of cubical type theory implemented by Agda --cubical, which is nice= ! Martin =20 > -Dan=20 > > > On Mar 8, 2019, at 9:59 AM, Anders Mortberg > wrote:=20 > >=20 > > In fact, in Cubical Agda you will not get these hcomp's with empty=20 > > systems. The reason is that because of the way hcomp works in Agda=20 > > there is a very nice trick to implement the "generalized hcomp"=20 > > operation of the paper that Dan linked to. I summarized the trick in:= =20 > >=20 > > https://github.com/agda/agda/issues/3415=20 > >=20 > > I added this to Agda some month ago and it should be possible to=20 > > update Simon's canonicity proof to get a stronger result saying that=20 > > the only elements of HITs in the empty context are point constructors= =20 > > (like in the AFH paper). For this to work you also have to impose a=20 > > "validity" constraint (Def 12 in the ccctt paper Dan linked to) so=20 > > that empty systems cannot result from substitutions. This is currently= =20 > > not done in Cubical Agda, but if you start with a term with only valid= =20 > > systems then you should never get an empty system.=20 > >=20 > > So the extraction of witnesses from existence statements should work=20 > > as Mart=C3=ADn said in Cubical Agda.=20 > >=20 > > --=20 > > Anders=20 > >=20 > > On Thu, Mar 7, 2019 at 6:23 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3=20 > > > wrote:=20 > >>=20 > >> And this is a wildly speculative question. If we used Andrew Swan's=20 > identity type derived from the cubical path type only, as in the abstract= =20 > library file=20 > https://github.com/agda/cubical/blob/master/Cubical/Core/HoTT-UF.agda)=20 > would we still get this phenomenon? Maybe not? What I mean is that we use= =20 > normal Agda, together with what is offered in that file and nothing else= =20 > (so that we are using HoTT book axiomatic type theory). Martin=20 > >>=20 > >> On Thursday, 7 March 2019 23:01:33 UTC, Mart=C3=ADn H=C3=B6tzel Escard= =C3=B3 wrote:=20 > >>>=20 > >>> Oh, this is annoying, because it seems to mean that we would need=20 > unbounded search (to drop all "hcom []"'s) until we can read the |x,a|,= =20 > which is against the spirit of, say, Martin-Loef type theories. Martin=20 > >>>=20 > >>> On Thursday, 7 March 2019 22:51:20 UTC, dlicata wrote:=20 > >>>>=20 > >>>> That would be true if the term you are normalizing is in the empty= =20 > interval context, and the cubical type theory has =E2=80=9Cempty system r= egularity=E2=80=9D=20 > (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf).=20 > >>>>=20 > >>>> Otherwise, if you evaluate something in the empty interval context,= =20 > you might see something like=20 > >>>> hcom [] (hcom [] (hcom [] (hcom [] (=E2=80=A6 |x,a| =E2=80=A6 ))))= =20 > >>>> with |x,a| in there somewhere. In HITs, Kan composition is treated= =20 > as a constructor of the type, and though there are no interesting lines t= o=20 > compose in the empty interval context, the uninteresting compositions don= =E2=80=99t=20 > vanish in all flavors of cubical type theory.=20 > >>>>=20 > >>>>> On Mar 7, 2019, at 5:41 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 < > escardo...@gmail.com> wrote:=20 > >>>>>=20 > >>>>> So I presume that when we ask cubical Agda to normalize a term of= =20 > type || Sigma (x:X), A x || we will get a term of the form |x,a| and so w= e=20 > will see the x in normal form, where |-| is the map into the truncation,= =20 > right? Martin.=20 > >>>>>=20 > >>>>> On Thursday, 7 March 2019 21:52:12 UTC, Anders M=C3=B6rtberg wrote:= =20 > >>>>> The existence property is proved for CCHM cubicaltt by Simon in:=20 > >>>>>=20 > >>>>> https://arxiv.org/abs/1607.04156=20 > >>>>>=20 > >>>>> See corollary 5.2. This works a bit more generally than what Mart= =C3=ADn=20 > said, in particular in any context with only dimension variables we can= =20 > compute a witness to an existence. So if in context G =3D i_1 : II, ..., = i_n=20 > : II (possibly empty) we have:=20 > >>>>>=20 > >>>>> G |- t : exists (x : X), A(x)=20 > >>>>>=20 > >>>>> then we can compute G |- u : X so that G |- B(u).=20 > >>>>>=20 > >>>>> --=20 > >>>>> Anders=20 > >>>>>=20 > >>>>> On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, Mart=C3=ADn H=C3= =B6tzel=20 > Escard=C3=B3 wrote:=20 > >>>>> I got confused now. :-)=20 > >>>>>=20 > >>>>> Seriously now, what you say seems related to the fact that from a= =20 > proof |- t : || X || in the empty context, you get |- x : X in cubical ty= pe=20 > theory. This follows from Simon's canonicity result (at least for X=3Dnat= ural=20 > numbers), and is like the so-called "existence property" in the internal= =20 > language of the free elementary topos. This says that from a proof |-=20 > exists (x:X), A x in the empty context, you get |- x : X and |- A x. This= =20 > says that exists in the empty context behaves like Sigma. But only in the= =20 > empty context, because otherwise it behaves like "local existence" as in= =20 > Kripke-Joyal semantics.=20 > >>>>>=20 > >>>>> Martin=20 > >>>>>=20 > >>>>> On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote:=20 > >>>>> Just in case anyone reading this thread later is confused about a= =20 > more beginner point than the ones Nicolai and Martin made, one possible= =20 > stumbling block here is that, if someone means =E2=80=9Cis inhabited=E2= =80=9D in an=20 > external sense (there is a closed term of that type), then the answer is= =20 > yes (at least in some models): if ||A|| is inhabited then A is inhabited.= =20 > For example, in cubical models with canonicity, it is true that a closed= =20 > term of type ||A|| evaluates to a value that has as a subterm a closed te= rm=20 > of type A (the other values of ||A|| are some =E2=80=9Cformal composition= s=E2=80=9D of=20 > values of ||A||, but there has to be an |a| in there at the base case).= =20 > This is consistent with what Martin and Nicolai said because =E2=80=9Cif= A is=20 > inhabited then B is inhabited=E2=80=9D (in this external sense) doesn=E2= =80=99t necessarily=20 > mean there is a map A -> B internally.=20 > >>>>>=20 > >>>>> -Dan=20 > >>>>>=20 > >>>>>> On Mar 5, 2019, at 6:07 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 < > escardo...@gmail.com> wrote:=20 > >>>>>>=20 > >>>>>> Or you can read the paper https://lmcs.episciences.org/3217/=20 > regarding what Nicolai said.=20 > >>>>>>=20 > >>>>>> Moreover, in the HoTT book, it is shown that if || X||->X holds fo= r=20 > all X, then univalence can't hold. (It is global choice, which can't be= =20 > invariant under equivalence.)=20 > >>>>>>=20 > >>>>>> The above paper shows that unrestricted ||X||->X it gives excluded= =20 > middle.=20 > >>>>>>=20 > >>>>>> However, for a lot of kinds of types one can show that ||X||->X=20 > does hold. For example, if they have a constant endo-function. Moreover,= =20 > for any type X, the availability of ||X||->X is logically equivalent to t= he=20 > availability of a constant map X->X (before we know whether X has a point= =20 > or not, in which case the availability of a constant endo-map is trivial)= .=20 > >>>>>>=20 > >>>>>> Martin=20 > >>>>>>=20 > >>>>>> On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote:=20 > >>>>>> You can't have a function which, for all A, gives you ||A|| -> A.= =20 > See the exercises 3.11 and 3.12!=20 > >>>>>> -- Nicolai=20 > >>>>>>=20 > >>>>>> On 05/03/19 22:31, Jean Joseph wrote:=20 > >>>>>>> Hi,=20 > >>>>>>>=20 > >>>>>>> From the HoTT book, the truncation of any type A has two=20 > constructors:=20 > >>>>>>>=20 > >>>>>>> 1) for any a : A, there is |a| : ||A||=20 > >>>>>>> 2) for any x,y : ||A||, x =3D y.=20 > >>>>>>>=20 > >>>>>>> I get that if A is inhabited, then ||A|| is inhabited by (1). But= =20 > is it true that, if ||A|| is inhabited, then A is inhabited?=20 > >>>>>>> --=20 > >>>>>>> You received this message because you are subscribed to the Googl= e=20 > Groups "Homotopy Type Theory" group.=20 > >>>>>>> To unsubscribe from this group and stop receiving emails from it,= =20 > send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com=20 > .=20 > >>>>>>> For more options, visit https://groups.google.com/d/optout.=20 > >>>>>>=20 > >>>>>>=20 > >>>>>> --=20 > >>>>>> You received this message because you are subscribed to the Google= =20 > Groups "Homotopy Type Theory" group.=20 > >>>>>> To unsubscribe from this group and stop receiving emails from it,= =20 > send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com=20 > .=20 > >>>>>> For more options, visit https://groups.google.com/d/optout.=20 > >>>>>=20 > >>>>>=20 > >>>>> --=20 > >>>>> You received this message because you are subscribed to the Google= =20 > Groups "Homotopy Type Theory" group.=20 > >>>>> To unsubscribe from this group and stop receiving emails from it,= =20 > send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com=20 > .=20 > >>>>> For more options, visit https://groups.google.com/d/optout.=20 > >>>>=20 > >> --=20 > >> You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group.=20 > >> To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com = .=20 > > >> For more options, visit https://groups.google.com/d/optout.=20 > > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_1410_162976777.1552084138226 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Friday, 8 March 2019 15:13:14 UTC, dlicata wro= te:
nice! the negation trick is= clever.=C2=A0

Yes, this is really nice= .

Martin, = I don=E2=80=99t understand why this situation is any different than natural= numbers, though. =C2=A0If I have a closed term of type nat, I can normaliz= e it, but then I (externally) need to read through all of the successors to= figure out what number it is. =C2=A0(Or maybe I can only weak head normali= ze it, in which case I need to interleave further weak head normalization a= fter every successor.) =C2=A0Is this an unbounded search? =C2=A0The paralle= l is to read =E2=80=9Chcom []=E2=80=9D as successor and =E2=80=9C|x,a|=E2= =80=9D as zero. =C2=A0


Except that you would have different n= ormal forms for the same thing, and this thing would be prefixed by an unbo= unded number of *printed* clock ticks.=C2=A0

It is= not right to say that unbounded search is needed, I agree. But it wouldn&#= 39;t be pleasant to have to see 10^6 ticks. I would rather wait for 10^6 un= its of time (which should be fast) and then see the answer than see=C2=A0 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 --cubica= l, which is nice!

Martin
=C2=A0
-Dan

> On Mar 8, 2019, at 9:59 AM, Anders Mortberg <andersm...@gmail.com> wrote:
>=20
> In fact, in Cubical Agda you will not get these hcomp's with e= mpty
> systems. The reason is that because of the way hcomp works in Agda
> there is a very nice trick to implement the "generalized hcom= p"
> operation of the paper that Dan linked to. I summarized the trick = in:
>=20
> https://github.com= /agda/agda/issues/3415
>=20
> I added this to Agda some month ago and it should be possible to
> update Simon's canonicity proof to get a stronger result sayin= g that
> the only elements of HITs in the empty context are point construct= ors
> (like in the AFH paper). For this to work you also have to impose = a
> "validity" constraint (Def 12 in the ccctt paper Dan lin= ked to) so
> that empty systems cannot result from substitutions. This is curre= ntly
> not done in Cubical Agda, but if you start with a term with only v= alid
> systems then you should never get an empty system.
>=20
> So the extraction of witnesses from existence statements should wo= rk
> as Mart=C3=ADn said in Cubical Agda.
>=20
> --
> Anders
>=20
> On Thu, Mar 7, 2019 at 6:23 PM Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3
> <escardo...@gmail.com> wrote:
>>=20
>> And this is a wildly speculative question. If we used Andrew S= wan'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 t= hat file and nothing else (so that we are using HoTT book axiomatic type th= eory). Martin
>>=20
>> On Thursday, 7 March 2019 23:01:33 UTC, Mart=C3=ADn H=C3=B6tze= l Escard=C3=B3 wrote:
>>>=20
>>> Oh, this is annoying, because it seems to mean that we wou= ld need unbounded search (to drop all "hcom []"'s) until we c= an read the |x,a|, which is against the spirit of, say, Martin-Loef type th= eories. Martin
>>>=20
>>> On Thursday, 7 March 2019 22:51:20 UTC, dlicata wrote:
>>>>=20
>>>> That would be true if the term you are normalizing is = in the empty interval context, and the cubical type theory has =E2=80=9Cemp= ty system regularity=E2=80=9D (like https://www.cs.cmu.edu/~cangiuli/paper= s/ccctt.pdf).
>>>>=20
>>>> Otherwise, if you evaluate something in the empty inte= rval context, you might see something like
>>>> hcom [] (hcom [] (hcom [] (hcom [] (=E2=80=A6 |x,a| = =E2=80=A6 ))))
>>>> with |x,a| in there somewhere. =C2=A0In HITs, Kan comp= osition is treated as a constructor of the type, and though there are no in= teresting lines to compose in the empty interval context, the uninteresting= compositions don=E2=80=99t vanish in all flavors of cubical type theory.
>>>>=20
>>>>> On Mar 7, 2019, at 5:41 PM, Mart=C3=ADn H=C3=B6tze= l Escard=C3=B3 <escardo...@gmail.com> wrote:
>>>>>=20
>>>>> So I presume that when we ask cubical Agda to norm= alize 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 th= e truncation, right? Martin.
>>>>>=20
>>>>> On Thursday, 7 March 2019 21:52:12 UTC, Anders M= =C3=B6rtberg wrote:
>>>>> The existence property is proved for CCHM cubicalt= t by Simon in:
>>>>>=20
>>>>> https://arxiv.org/abs/1607.04= 156
>>>>>=20
>>>>> See corollary 5.2. This works a bit more generally= than what Mart=C3=ADn said, in particular in any context with only dimensi= on variables we can compute a witness to an existence. So if in context G = =3D i_1 : II, ..., i_n : II =C2=A0(possibly empty) =C2=A0we have:
>>>>>=20
>>>>> G |- t : exists (x : X), A(x)
>>>>>=20
>>>>> then we can compute G |- u : X so that G |- B(u).
>>>>>=20
>>>>> --
>>>>> Anders
>>>>>=20
>>>>> On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, M= art=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote:
>>>>> I got confused now. :-)
>>>>>=20
>>>>> Seriously now, what you say seems related to the f= act 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 (a= t least for X=3Dnatural 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 lik= e Sigma. But only in the empty context, because otherwise it behaves like &= quot;local existence" as in Kripke-Joyal semantics.
>>>>>=20
>>>>> Martin
>>>>>=20
>>>>> On Thursday, 7 March 2019 14:10:56 UTC, dlicata wr= ote:
>>>>> Just in case anyone reading this thread later is c= onfused about a more beginner point than the ones Nicolai and Martin made, = one possible stumbling block here is that, if someone means =E2=80=9Cis inh= abited=E2=80=9D 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 th= en A is inhabited. =C2=A0For 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 =E2= =80=9Cformal compositions=E2=80=9D of values of ||A||, but there has to be = an |a| in there at the base case). =C2=A0This is consistent with what Marti= n and Nicolai said because =E2=80=9Cif A is inhabited then B is inhabited= =E2=80=9D (in this external sense) doesn=E2=80=99t necessarily mean there i= s a map A -> B internally.
>>>>>=20
>>>>> -Dan
>>>>>=20
>>>>>> On Mar 5, 2019, at 6:07 PM, Mart=C3=ADn H=C3= =B6tzel Escard=C3=B3 <escardo...@gmail.com> wrote:
>>>>>>=20
>>>>>> Or you can read the paper https://lmcs.episciences.org/3217/ regarding what Nicolai said= .
>>>>>>=20
>>>>>> Moreover, in the HoTT book, it is shown that i= f || X||->X holds for all X, then univalence can't hold. (It is glob= al choice, which can't be invariant under equivalence.)
>>>>>>=20
>>>>>> The above paper shows that unrestricted ||X||-= >X it gives excluded middle.
>>>>>>=20
>>>>>> However, for a lot of kinds of types one can s= how that ||X||->X does hold. For example, if they have a constant endo-f= unction. Moreover, for any type X, the availability of ||X||->X is logic= ally equivalent to the availability of a constant map X->X (before we kn= ow whether X has a point or not, in which case the availability of a consta= nt endo-map is trivial).
>>>>>>=20
>>>>>> Martin
>>>>>>=20
>>>>>> 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
>>>>>>=20
>>>>>> On 05/03/19 22:31, Jean Joseph wrote:
>>>>>>> Hi,
>>>>>>>=20
>>>>>>> From the HoTT book, the truncation of any = type A has two constructors:
>>>>>>>=20
>>>>>>> 1) for any a : A, there is |a| : ||A||
>>>>>>> 2) for any x,y : ||A||, x =3D y.
>>>>>>>=20
>>>>>>> I get that if A is inhabited, then ||A|| i= s inhabited by (1). But is it true that, if ||A|| is inhabited, then A is i= nhabited?
>>>>>>> --
>>>>>>> You received this message because you are = subscribed to the Google Groups "Homotopy Type Theory" group.
>>>>>>> To unsubscribe from this group and stop re= ceiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@goo= glegroups.com.
>>>>>>> For more options, visit https://groups.google.com/d/optout.
>>>>>>=20
>>>>>>=20
>>>>>> --
>>>>>> You received this message because you are subs= cribed to the Google Groups "Homotopy Type Theory" group.
>>>>>> To unsubscribe from this group and stop receiv= ing emails from it, send an email to HomotopyTypeTheory+unsubscribe@googleg= roups.com.
>>>>>> For more options, visit https://groups.google.com/d/optout.
>>>>>=20
>>>>>=20
>>>>> --
>>>>> You received this message because you are subscrib= ed 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@googlegroup= s.com.
>>>>> For more options, visit = https://groups.google.com/d/optout.
>>>>=20
>> --
>> You received this message because you are subscribed to the Go= ogle 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://group= s.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_1410_162976777.1552084138226-- ------=_Part_1409_1448670496.1552084138225--