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-oi1-x237.google.com (mail-oi1-x237.google.com [IPv6:2607:f8b0:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3800437c for ; Thu, 7 Mar 2019 23:23:42 +0000 (UTC) Received: by mail-oi1-x237.google.com with SMTP id q82sf9047337oia.9 for ; Thu, 07 Mar 2019 15:23:42 -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=jKhSt/fS2Vbh6FmH873TXx5IE9OL8W6qthzIomNeYfI=; b=OgLQVt2Dkb1+Qh/42h0DP/qixIyIjuxt2KO9VAurBzdm482TLXyYU9c8Eo7BWWD4nS 472BeSR2LH1MKLBO4sN6533z76MzdNAbgKTnqZ0sPBnMPf7p2jk6azf+0qeOsdtrcj92 b1MZrXDAPs++a5Xjr1z07Jo2qdGSn/IINEsxsOJMrWCJCd7voVQO1g+O3VUWB20R+yuN B/IL7lewHK2fiky7TjQanmIRcsZOlyKnu2PvWSZTmEkaEC/GPisQa5umiWtnSPKSW5fg YsmxEdUV8bkbHub+krqZWNnFTqxgBz2JETa5xpxTDmmHno+y1rmp7Rah2KmbPVc/5kZq N/gA== 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=jKhSt/fS2Vbh6FmH873TXx5IE9OL8W6qthzIomNeYfI=; b=Si262sRMNGYhAjPtN3Bht6GzkjJ+DGbztPeockAFq41e6fdBpy0ghGUf7qffGR3eig 5Kng+TKeU3OAtUNAVn6ILhj6qCmzym+l9Jl/RFdWUxCUAS+K5hsQGITw+c1FrHFoeBui rBRHt2nR726/0ei7MxQU/r8M6iwf4+b4xvbueM/YQCu16rNyABsiGeTSvMV+3D0ufSsF BxP42rq2k89n8ZpBq0pbTRXSFTzVLm6dF+jV5L85gRAE2OrGCn8CqbXRgSU4TA0Vucaq p8fgDfF0MObIssTA5L5Ch1xNsuL1f+hpHIFw1PHY1bdRxYFBqq4U8Q79R1zh8RxIGwf3 og4w== 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=jKhSt/fS2Vbh6FmH873TXx5IE9OL8W6qthzIomNeYfI=; b=gYYOXj6ruzj+4bBemLZJgR/j2AhKw4JiZsArQj+zZYrroG8iil1bOp3kRIdZ8PKDJR UhmeRI4M2dqrM8cPfGclzvF21Lp0pc86nN6AsE2JllH9jRxwYINZO+9s3lyfPDfLtCW/ VgPW7+hs1oslTLakzkR7yU24jlVckGTUJOcemSFpKQzWgBsOJpmZzHdo1Rypjsc+EqKT JO5O9Gh0+RkeMY4/jQs4BQRTjfkKDHl95/ecS+XLXCGpboV8KPGJPSAuc6nIaiIOmyEn jx7C+FbpLmEuX33V5FL0Wmaw7p65tJkinCk7fHxfZHIYf39RTaJy4NU2nFR+Io4Li4p4 coQg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXhLL3NuDz7dvVyyFXuU8AmAl+jPg9vAUTFtBfnC8fYqsKfCWaj LjZBDsuBz0Qf6rq19cVlsmw= X-Google-Smtp-Source: APXvYqwZPRYWE1w/mSqYgvrBH+eb5g6rjCAYsL2T2NukILdgRjaWUfSNCPwKzxpyRE3h2EL4k6wmhA== X-Received: by 2002:a9d:6355:: with SMTP id y21mr10268621otk.6.1552001021366; Thu, 07 Mar 2019 15:23:41 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:b446:: with SMTP id d67ls1623514oif.3.gmail; Thu, 07 Mar 2019 15:23:40 -0800 (PST) X-Received: by 2002:aca:5143:: with SMTP id f64mr6685670oib.137.1552001020293; Thu, 07 Mar 2019 15:23:40 -0800 (PST) Date: Thu, 7 Mar 2019 15:23:39 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <7a7c3e3f-df35-42ea-9d89-f0d20b855e9e@googlegroups.com> In-Reply-To: <50111384-09a4-4c30-8272-fa9e5997d3c3@googlegroups.com> 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> Subject: Re: [HoTT] Propositional Truncation MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1026_1703241282.1552001019672" 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_1026_1703241282.1552001019672 Content-Type: multipart/alternative; boundary="----=_Part_1027_496967448.1552001019672" ------=_Part_1027_496967448.1552001019672 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 On Thursday, 7 March 2019 23:01:33 UTC, Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3 wrote: > > 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 > > 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=20 >> interval context, and the cubical type theory has =E2=80=9Cempty system = regularity=E2=80=9D=20 >> (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf). =20 >> >> Otherwise, if you evaluate something in the empty interval context, you= =20 >> 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 as a= =20 >> constructor of the type, and though there are no interesting lines to=20 >> compose in the empty interval context, the uninteresting compositions do= n=E2=80=99t=20 >> vanish in all flavors of cubical type theory. =20 >> >> > On Mar 7, 2019, at 5:41 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 =20 >> wrote:=20 >> >=20 >> > So I presume that when we ask cubical Agda to normalize a term of type= =20 >> || Sigma (x:X), A x || we will get a term of the form |x,a| and so we wi= ll=20 >> see the x in normal form, where |-| is the map into the truncation, righ= t?=20 >> 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=B6tz= el Escard=C3=B3=20 >> wrote:=20 >> > I got confused now. :-)=20 >> >=20 >> > Seriously now, what you say seems related to the fact that from a proo= f=20 >> |- t : || X || in the empty context, you get |- x : X in cubical type=20 >> theory. This follows from Simon's canonicity result (at least for X=3Dna= tural=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. Thi= s=20 >> says that exists in the empty context behaves like Sigma. But only in th= e=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 more= =20 >> 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 close= d=20 >> term of type ||A|| evaluates to a value that has as a subterm a closed t= erm=20 >> of type A (the other values of ||A|| are some =E2=80=9Cformal compositio= ns=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=9Ci= f 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 for= =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 does= =20 >> hold. For example, if they have a constant endo-function. Moreover, for = any=20 >> type X, the availability of ||X||->X is logically equivalent to the=20 >> availability of a constant map X->X (before we know whether X has a poin= t=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. Se= e=20 >> 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 i= s=20 >> it true that, if ||A|| is inhabited, then A is inhabited?=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 >> > >> 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 >> > > 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, 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_1027_496967448.1552001019672 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
And this is a wildly speculative question. If we used Andr= ew Swan's identity type derived from the cubical path type only, as in = the abstract library file https://github.com/agda/cubical/blob/master/Cubic= al/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 fil= e and nothing else (so that we are using HoTT book axiomatic type theory). = Martin

On Thursday, 7 March 2019 23:01:33 UTC, Mart=C3=ADn H=C3=B6tz= el Escard=C3=B3 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 n= ormalizing is in the empty interval context, and the cubical type theory ha= s =E2=80=9Cempty system regularity=E2=80=9D (like https://www.cs.cmu.edu/~= cangiuli/papers/ccctt.pdf). =C2=A0=20

Otherwise, if you evaluate something in the empty interval 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 composition is treate= d as a constructor of the type, and though there are no interesting lines t= o compose in the empty interval context, the uninteresting compositions don= =E2=80=99t vanish in all flavors of cubical type theory. =C2=A0

> On Mar 7, 2019, at 5:41 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 &= lt;escardo...@gmail.com> wrote:
>=20
> 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, ri= ght? Martin.
>=20
> On Thursday, 7 March 2019 21:52:12 UTC, Anders M=C3=B6rtberg wrote= :
> The existence property is proved for CCHM cubicaltt by Simon in:
>=20
> https://arxiv.org/abs/1607.04156
>=20
> See corollary 5.2. This works a bit more generally than what Mart= =C3=ADn said, in particular in any context with only dimension 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, Mart=C3=ADn H=C3= =B6tzel Escard=C3=B3 wrote:
> I got confused now. :-)
>=20
> 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=3D= 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 onl= y in the empty context, because otherwise it behaves like "local exist= ence" as in Kripke-Joyal semantics.=20
>=20
> Martin
>=20
> 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 stu= mbling block here is that, if someone means =E2=80=9Cis inhabited=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 then A is inhabite= d. =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 clos= ed term of type A (the other values of ||A|| are some =E2=80=9Cformal compo= sitions=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 Martin and Nicolai said= because =E2=80=9Cif A is inhabited then B is inhabited=E2=80=9D (in this e= xternal sense) doesn=E2=80=99t necessarily mean there is a map A -> B in= ternally. =C2=A0=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/ regarding what Nicolai said.=20
> >=20
> > 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, whic= h can't be invariant under equivalence.)=20
> >=20
> > The above paper shows that unrestricted ||X||->X it gives = excluded middle.=20
> >=20
> > 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. Moreov= er, 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 ha= s a point 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. 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 = 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 is it true that, if ||A|| is inhabited, then A is inhabited?=20
> >> --=20
> >> You received this message because you are subscribed to t= he Google Groups "Homotopy Type Theory" group.=20
> >> To unsubscribe from this group and stop receiving emails = from it, send an email to HomotopyTypeTheory+unsub= scribe@googlegroups.com.=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 G= oogle Groups "Homotopy Type Theory" group.=20
> > To unsubscribe from this group and stop receiving emails from= it, send an email to HomotopyTypeTheory+unsubscri= be@googlegroups.com.=20
> > For more options, visit https://grou= ps.google.com/d/optout.=20
>=20
>=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 email to HomotopyTypeTheory+unsubscribe@go= oglegroups.com.
> For more options, visit https://groups.go= ogle.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_1027_496967448.1552001019672-- ------=_Part_1026_1703241282.1552001019672--