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.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,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-io1-xd3d.google.com (mail-io1-xd3d.google.com [IPv6:2607:f8b0:4864:20::d3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f208ba72 for ; Thu, 7 Mar 2019 16:35:30 +0000 (UTC) Received: by mail-io1-xd3d.google.com with SMTP id k24sf13064535ioa.18 for ; Thu, 07 Mar 2019 08:35:30 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1551976529; cv=pass; d=google.com; s=arc-20160816; b=ybNjLN+KdbV7E5oqLcIzrfVrA3HyURs0lVMfbirg/5zY8e4BNp4S/gLLgPBBpiGIWp Ouafmoiw5EFR3WKSEvV/RsJWqL7LlJ6XLEPzq1/8CLksZeGzQLEQrrdvt6nk5TKPWUtL S9reHVxeNanpd5lyyAk4i/grTdayqZ1gI1i1ZQWhPj73TSL6yRj+vsOAsVCzUnNC+0Da 6+kJorTF1cE+EEa73NcrHJU43986s0sk23G5pCs0xta255ucVlPHe1dy1Ev89oVtmUxB Kf8ZsXtnYgY3/UvKW9qMGpCM25mOUku+rK/APrC2qLURps9XOL0EZPDHaB/FyTyQO1rs /2Cg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:references:to:cc:in-reply-to:date:subject :mime-version:message-id:from:sender:dkim-signature; bh=kpirE95RwjUp4MqTkSR8EkxmdWY2pKOSCOQagW0Ss7U=; b=nRnT54H81SHnG96DRjT9+pFF5WJlOms2UXcC2V83mlexjn1kIqBb5Nu+WzIfSD6bFs pAfVtQnyiDOBP76If4tnlII46tggqpz1souG1LUMmtP2qQsRgEVD+pyZJR3bWaYdSPXv rbgifBs9kT3T0NSrgoXr7GzVOcEkViaJJAAT/Tax8ISWSi38PwUSYvNtfc0sxD2LdPB2 C5m2SE88y788YfTRquHuIT4/xrFTmNBzNql/MR61jCql3PczZXlQolUg5bUiTS5rxaV6 8nKOAKar6RfveZJZwICeU9E26gfYwrA4IbAhjTaEJEN4/UXifQGZA6IsTqhN1xTMKWId 3QdA== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of sherman@csail.mit.edu designates 128.30.2.210 as permitted sender) smtp.mailfrom=sherman@csail.mit.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=csail.mit.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:message-id:mime-version:subject:date:in-reply-to:cc:to :references:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=kpirE95RwjUp4MqTkSR8EkxmdWY2pKOSCOQagW0Ss7U=; b=NVH0uH81XBNAMf7c+VqY1y9TzG9ZmofOdCGmSgrFUtWpmIt1/LZ4SuMJapoy1ySC3M MUS6HQq2cwEUAhy5m7O6Ai41iR1aqlaIaqJKY+7E8WOkoSKqUh86otyuhyilAVm6AxVH Kpq/o1yJcyUh4F/2/xip6IGwQyOFuHGpxD/O63Snq78QDcZ80E89DwekkJqqEfEDl7a8 9JA3kemnITZU7cDtU4FtBCjU+wN+Xyf9pnfDi3dPXbx6s7jmnitOQlet69+nsURrvDs7 07jkyhNun+FkshdgMKZFCZqPRqZDWVUmOCyu82Lbf+V5Iy0NYlbV1mSditSDaBOAebzW dIww== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:message-id:mime-version:subject:date :in-reply-to:cc:to:references:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=kpirE95RwjUp4MqTkSR8EkxmdWY2pKOSCOQagW0Ss7U=; b=AhcuO0Lsdid9UhZaXcbm94kz6L7aiFxmKjwLzX9HX1rKXbrPEA4bBheisxmhqE0Pu7 s+sa4nWOS3d6Q4AHSiYYfzzT93GJEX3+KSdj1XjvgUK4CEcnAwrRRiAUCHR+oh+Krap5 QE+wTX+P+nq6wGZMOcxlEb7TvIvGOyat/HV9c0+BKIwz3fcWs27FEECElQ0W+QITgFkn Mubyjem7iE65F/AZweg9yJT9ylB5w16+OrUBmXJcCO6EUvVUVLmCg13oKh2FZWVE4+QE DmSEo7CuyuY8UZTt+NOzvqeTfolJv3TGraYlVnLSD2lfuC2HW9yo56vVqhhK48r/DZcs E0cw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVv+aoxXS/kwXuXA2UTZb+MTJyjqOAHYb1dYED3QWw67BhsdHwy Yhv+0Mf+y5HDFimbAY4GQoM= X-Google-Smtp-Source: APXvYqxC0r8ZG1VMiQfBc4st4OwPexhA2s6KmUvhAu4909DoGu2qBhx4S6bJbfWswokp9yqICEz4YA== X-Received: by 2002:a5d:8701:: with SMTP id u1mr7181927iom.69.1551976529800; Thu, 07 Mar 2019 08:35:29 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:8154:: with SMTP id f20ls2429746ioo.2.gmail; Thu, 07 Mar 2019 08:35:29 -0800 (PST) X-Received: by 2002:a5d:819a:: with SMTP id u26mr8040123ion.20.1551976529399; Thu, 07 Mar 2019 08:35:29 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1551976529; cv=none; d=google.com; s=arc-20160816; b=cProTyUihPgq4URgIhciQWWHMNJ0Ts1NieW593d/NH3k3SgNmVghHHlFOuv3DPJG8p lSdued3lnMjCUKr7FQuVi98NJGN5xoMXvx9yVWmVYqOGUGrJ20ZbfiEm76h317RJflpt 8WWYKLxttFycVC6El7nNSB5ilf8DnQYkTkD6ZNDTEjCTRNj69GsQa+7C4uNCqeoL5JX8 QxKLknBv7nIxLKlATZA/tfVTfS3RwxqoCgheP+HOZLBYBR3krKeTJMsTfpSiqS+RYEvr XIQ7le2feMqIbty5cFQe1FqvzHYo0mKfoL7J90Kn094ImKcl8WSvoCy1hcAKsPK/7aLh O6JQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from; bh=I9ggchLdQSZIlefhxw++3acZjzN8oMTP1/KjMrSG1AI=; b=AoUIOiKPOrs0QyB3jrCYquJjU+heGOkk4/f7Y4PBKIu5NNvzLf/rwJ+lJ3MS3n0Jl9 gvylH+BId5XysPQmutAMkiTIds7WcBrDIJ3RxJrRRlN7mUiq19ezzpUhv5Y2IJDypbHr A/rW4nZVKHL7hkxe5H1VjWHWtnp2Tqy/jEFhQtdgLpZ1sh3d1CfS2wQS+hI5+D5W6Rlp pJPYTQCvjFdZ6BXrHjHuZwME/qiZdo1tn71CjzQvjIEwJvT81TROaTMrK5L5u0X6LlXE tWg5X3sYJaGivGbC/dQYXJYxqFT1YzkKxvdrTrXZXxyiiv/ENBsJW0+NJZ6hTOWVAgDO SiIA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of sherman@csail.mit.edu designates 128.30.2.210 as permitted sender) smtp.mailfrom=sherman@csail.mit.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=csail.mit.edu Received: from outgoing-stata.csail.mit.edu (outgoing-stata.csail.mit.edu. [128.30.2.210]) by gmr-mx.google.com with ESMTP id f19si210881iol.4.2019.03.07.08.35.29 for ; Thu, 07 Mar 2019 08:35:29 -0800 (PST) Received-SPF: pass (google.com: domain of sherman@csail.mit.edu designates 128.30.2.210 as permitted sender) client-ip=128.30.2.210; Received: from [18.40.43.159] by outgoing-stata.csail.mit.edu with esmtpsa (TLS1.2:DHE_RSA_AES_256_CBC_SHA256:256) (Exim 4.82) (envelope-from ) id 1h1vzU-0007YU-BM; Thu, 07 Mar 2019 11:35:28 -0500 From: Ben Sherman Message-Id: Content-Type: multipart/alternative; boundary="Apple-Mail=_F3C7956D-5F67-4C86-B488-CF5C94C4C319" Mime-Version: 1.0 (Mac OS X Mail 12.2 \(3445.102.3\)) Subject: Re: [HoTT] Propositional Truncation Date: Thu, 7 Mar 2019 11:35:15 -0500 In-Reply-To: <30ae0dc4-cef2-46ad-a280-bdf617a0db4e@googlegroups.com> Cc: Homotopy Type Theory To: =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= References: <0f5b8d0e-9f1d-47a7-9d39-a9112afb77ea@googlegroups.com> <12cd6b73-7ca6-481c-9503-250af28b8113@googlegroups.com> <30ae0dc4-cef2-46ad-a280-bdf617a0db4e@googlegroups.com> X-Mailer: Apple Mail (2.3445.102.3) X-Original-Sender: sherman@csail.mit.edu X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of sherman@csail.mit.edu designates 128.30.2.210 as permitted sender) smtp.mailfrom=sherman@csail.mit.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=csail.mit.edu 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: , --Apple-Mail=_F3C7956D-5F67-4C86-B488-CF5C94C4C319 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" On a similar note, I had originally (and mistakenly, at least according to = the terminology in the HoTT book, which I looked up) thought that declaring= =E2=80=9CA is inhabited=E2=80=9D rather than just =E2=80=9CA=E2=80=9D was = meant to refer to the type || A || rather than A, in which case, I read the= question =E2=80=9Cif || A || is inhabited, then A is inhabited=E2=80=9D as || || A || || -> || A || The above statement does hold, and in some way I think of this (though I=E2= =80=99m not sure how to connect it formally) as an internalization of Dan= =E2=80=99s and Martin=E2=80=99s external statements. (According to the HoTT book, we say =E2=80=9CA is merely inhabited=E2=80=9D= to say || A ||.) > On Mar 7, 2019, at 11:16 AM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: >=20 > 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=3Dnatural num= bers), and is like the so-called "existence property" in the internal langu= age 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 e= xists in the empty context behaves like Sigma. But only in the empty contex= t, because otherwise it behaves like "local existence" as in Kripke-Joyal s= emantics.=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 be= ginner point than the ones Nicolai and Martin made, one possible stumbling = block here is that, if someone means =E2=80=9Cis inhabited=E2=80=9D in an e= xternal 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 t= ype 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). This is consistent with 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. =20 >=20 > -Dan=20 >=20 > > On Mar 5, 2019, at 6:07 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 > 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, which can't be invari= ant under equivalence.)=20 > >=20 > > The above paper shows that unrestricted ||X||->X it gives excluded midd= le.=20 > >=20 > > However, for a lot of kinds of types one can show that ||X||->X does ho= ld. For example, if they have a constant endo-function. Moreover, for any t= ype X, the availability of ||X||->X is logically equivalent to the availabi= lity of a constant map X->X (before we know whether X has a point or not, i= n 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 t= he 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 i= t true that, if ||A|| is inhabited, then A is inhabited?=20 > >> --=20 > >> You received this message because you are subscribed to the Google Gro= ups "Homotopy Type Theory" group.=20 > >> To unsubscribe from this group and stop receiving emails from it, 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 Grou= ps "Homotopy Type Theory" group.=20 > > To unsubscribe from this group and stop receiving emails from it, 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 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 . --=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. --Apple-Mail=_F3C7956D-5F67-4C86-B488-CF5C94C4C319 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset="UTF-8"
On a similar note, I = had originally (and mistakenly, at least according to the terminology in th= e HoTT book, which I looked up) thought that declaring =E2=80=9CA is inhabi= ted=E2=80=9D rather than just =E2=80=9CA=E2=80=9D was meant to refer to the= type || A || rather than A, in which case, I read the question =E2=80=9Cif= || A || is inhabited, then A is inhabited=E2=80=9D as

|| || A || || -> || A ||

The above statement does hold, and in some way I think of this (thoug= h I=E2=80=99m not sure how to connect it formally) as an internalization of= Dan=E2=80=99s and Martin=E2=80=99s external statements.

(According to the HoTT book, we say =E2=80=9CA is merely inhabited=E2=80=9D to say || A ||.)

On Mar 7, 2019, = at 11:16 AM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 <escardo.martin@gmail.com> wrote:
I got confused now. :-)

Seriously now, what you say seems related to the fact that fr= om 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= =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. Th= is says that exists in the empty context behaves like Sigma. But only in th= e empty context, because otherwise it behaves like "local existence" as in = Kripke-Joyal semantics. 

Martin

On Thursday, 7 Marc= h 2019 14:10:56 UTC, dlicata wrote:
Just in case anyone reading this thread later is confused about a mor= e beginner point than the ones Nicolai and Martin made, one possible stumbl= ing 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 inhabited. =  For example, in cubical models with canonicity, it is true that a clo= sed 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 composit= ions=E2=80=9D of values of ||A||, but there has to be an |a| in there at th= e base case).  This is consistent with what Martin and Nicolai said be= cause =E2=80=9Cif A is inhabited then B is inhabited=E2=80=9D (in this exte= rnal sense) doesn=E2=80=99t necessarily mean there is a map A -> B inter= nally.  

-Dan

> On Mar 5, 2019, at 6:07 PM, Mart=C3=ADn H=C3=B6tzel Esc= ard=C3=B3 <escardo...@gmail.com> wrote:
>=20
> Or you can read the paper https://lmc= s.episciences.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, wh= ich can't be invariant under equivalence.)
>=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. = Moreover, for any type X, the availability of ||X||->X is logically equi= valent to the availability of a constant map X->X (before we know whethe= r X has a point or not, in which case the availability of a constant endo-m= ap is trivial).
>=20
> Martin
>=20
> On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wr= ote:
> 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 ha= s two constructors:
>>=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 inhabit= ed by (1). But is it true that, if ||A|| is inhabited, then A is inhabited?= =20
>> --=20
>> You received this message because you are subscribe= d to the Google Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving e= mails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
>> For more options, visit https://g= roups.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 email= s 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 "= 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.

--
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.
--Apple-Mail=_F3C7956D-5F67-4C86-B488-CF5C94C4C319--