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-x33f.google.com (mail-ot1-x33f.google.com [IPv6:2607:f8b0:4864:20::33f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0f699709 for ; Thu, 7 Mar 2019 22:41:16 +0000 (UTC) Received: by mail-ot1-x33f.google.com with SMTP id s12sf7909298oth.14 for ; Thu, 07 Mar 2019 14:41:16 -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=Dnf9p5HC7eC5XL0SXLQAK8rviiU+LZtkoHspQ4FyZl4=; b=achyJx6ic0AfLs7eBPDR2BOBmxQboBR1bCfYqSfTHp4JHk6bWMGjRFR/vmBLL+6rFL qn6Jpj5wxESNqi4zyQ/dmXMkDr3agXlYvCIBNdkT/TtYesqV4+f/AatnNFOJ59GRIML5 8Ztdmw1UytgsA/MDwWIlQsvDgT8txOueZg4kbF1OIsAM4jHaK/hDvD3lliK5VNchvd99 789fGB3mmuVLVj3UDxBGk4jURy2u5e4GTlOW7hdL36B51qDnV057fnvQVTAY1jXOEiPE f33PbY9BeCc9W5V+mbbsO1qRDDR8qPf0vzjBkf0XlmY2c3wTDzx9G2c9Itt1QowX20G8 +wTg== 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=Dnf9p5HC7eC5XL0SXLQAK8rviiU+LZtkoHspQ4FyZl4=; b=gX+EJzC38VBp+vKRxc21y5WFDZqJmMpZNRq4c2y7M+ilJ43rrSJuMTPPx7L825HX58 bTol3RoBnKNcuIZH/myY6tlE1H9yXl0kW19fMDIUrk54N1OQh4uuKbqSIPhEGmKBxMrG RDnJDvkEaCbkyWHTNGlA3C2sCF/w2oPZNDLg87ilRG+JlLtD1jRlq7p3cZFwbnSJ+sXc sem+c2cj+M3xl2izMiU8rQSofCyaIOMquoYRH7GtdJ4vHmh9eFeGyOwLfzdIY8bxYJ2Q ISMpalp/X8yNC9W8vYux1l/0zJyRuQ+m+QVXfho32WsYFdVti1ztHDb/QK31kVZaxJn3 l6sQ== 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=Dnf9p5HC7eC5XL0SXLQAK8rviiU+LZtkoHspQ4FyZl4=; b=oFIaC/TYZ+M+GIlglXZ1+w8B/E0EwqlZpU6QIB4b1bnHBD78GjKVT9me24D1nNgei8 ZcfCi6+YpJNrGgzFApNcGq0nV9vdA6ckdxKD3J3S3eYUMfme3gyeA9/RXugdn45jG04L cg0VSEcbH59VAo2yV+08duPbSLYCBfJdSLcKFXFpVT44L8rQsJqWf2KHerOEhX8qFp0b mnIz4/LXg/ytxUNEA0QFHDOxFmPYEkeF1HyN1dtCeHFbqLYwLWDJRC2h27t3L+LBj7cc uiOmqABCN8iXdh822HStiLxxHaxS4kI1AuIEUArMtEUnggOUH1Z5claOkpqvQ0dY7bhz Jvcw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWknCubhi1sHxpaamAWIOyNO/HaQNCS9SgOFjj3rjcrjA6YE5Y7 spgHxeGqAVpLAT5UTvsVBg8= X-Google-Smtp-Source: APXvYqwahrxE79W5Z13LuycrPVV8jK74/1vX+CqnRIcWwX/K5+Hv9NDtsHDZNXGZndRKVg2IAsEqOA== X-Received: by 2002:aca:4bd6:: with SMTP id y205mr6352260oia.43.1551998475702; Thu, 07 Mar 2019 14:41:15 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:5d11:: with SMTP id b17ls1471741oti.8.gmail; Thu, 07 Mar 2019 14:41:15 -0800 (PST) X-Received: by 2002:a9d:6348:: with SMTP id y8mr9398328otk.287.1551998474854; Thu, 07 Mar 2019 14:41:14 -0800 (PST) Date: Thu, 7 Mar 2019 14:41:14 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <5f7932a1-417b-42be-9d63-300dddc83037@googlegroups.com> In-Reply-To: <9fbd1c51-139e-4657-980a-2264a8f9ff92@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> Subject: Re: [HoTT] Propositional Truncation MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1046_1937365128.1551998474270" 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_1046_1937365128.1551998474270 Content-Type: multipart/alternative; boundary="----=_Part_1047_346762981.1551998474271" ------=_Part_1047_346762981.1551998474271 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 will see= =20 the x in normal form, where |-| is the map into the truncation, right?=20 Martin. 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: > > https://arxiv.org/abs/1607.04156 > > See corollary 5.2. This works a bit more generally than what Mart=C3=ADn = said,=20 > in particular in any context with only dimension variables we can compute= a=20 > witness to an existence. So if in context G =3D i_1 : II, ..., i_n : II = =20 > (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=C3=ADn H=C3=B6tzel = Escard=C3=B3=20 > wrote: >> >> I got confused now. :-) >> >> Seriously now, what you say seems related to the fact that from a proof= =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 >> >> 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= =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 i= s=20 >>> yes (at least in some models): if ||A|| is inhabited then A is inhabite= d.=20 >>> For example, in cubical models with canonicity, it is true that a clos= ed=20 >>> term of type ||A|| evaluates to a value that has as a subterm a closed = term=20 >>> of type A (the other values of ||A|| are some =E2=80=9Cformal compositi= ons=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=9C= if 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 >>> >>> -Dan=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 poi= nt=20 >>> or not, in which case the availability of a constant endo-map is trivia= l).=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= =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 is= =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, sen= d=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_1047_346762981.1551998474271 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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| an= d so we will see the x in normal form, where |-| is the map into the trunca= tion, right? Martin.

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:


See corollary 5.2. This works a bit mo= re 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=A0 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 1= 1:16:48 AM UTC-5, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 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 ty= pe theory. This follows from Simon's canonicity result (at least for X= =3Dnatural numbers), and is like the so-called "existence property&quo= t; in the internal language of the free elementary topos. This says that fr= om 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 ex= istence" as in Kripke-Joyal semantics.=C2=A0

= Martin

On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote= :
Just in case anyone reading this t= hread later is confused about a more beginner point than the ones Nicolai a= nd Martin made, one possible stumbling block here is that, if someone means= =E2=80=9Cis inhabited=E2=80=9D in an external sense (there is a closed ter= m of that type), then the answer is yes (at least in some models): if ||A||= is inhabited then A is inhabited. =C2=A0For example, in cubical models wit= h canonicity, it is true that a closed term of type ||A|| evaluates to a va= lue 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 th= ere has to be an |a| in there at the base case). =C2=A0This is consistent w= ith what Martin 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 is a map A -> B internally. =C2=A0

-Dan

> On Mar 5, 2019, at 6:07 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 &= lt;escardo...@gmail.com> wrote:
>=20
> Or you can read the paper https://lmcs.episc= iences.org/3217/ regarding what Nicolai said.
>=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, which can= 't be invariant under equivalence.)
>=20
> The above paper shows that unrestricted ||X||->X it gives exclu= ded 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. Moreover, f= or any type X, the availability of ||X||->X is logically equivalent to t= he availability of a constant map X->X (before we know whether X has a p= oint or not, in which case the availability of a constant endo-map is trivi= al).
>=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|| -&= gt; 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 const= ructors:
>>=20
>> 1) for any a : A, there is |a| : ||A||
>> 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 the Go= ogle Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from = it, send an email to HomotopyTypeTheory+unsubscrib= e@googlegroups.com.
>> For more options, visit https://group= s.google.com/d/optout.
>=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_1047_346762981.1551998474271-- ------=_Part_1046_1937365128.1551998474270--