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-x337.google.com (mail-ot1-x337.google.com [IPv6:2607:f8b0:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f8988cfc for ; Thu, 7 Mar 2019 16:16:51 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id r22sf7333582otk.1 for ; Thu, 07 Mar 2019 08:16:50 -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=pnogRv6P2EdhZlVXH4Z31eC8bqrWUx0N9Dr5suFDyHA=; b=PTHx3giMzvnAdfOFJNh8Xsg9V7elHWeGxAV7OsbZUgLp3iSeQ9BUHCzHN17WKih3+e OBOvFyO0B+DqepHmpJyqTd6yh60M/qXVKLF3cSHwK8xDYdqCLoi0e3P1PIiwfeFXvJJy BDf0ibxhn/It32zQc1SsbOJjJ09FCGhT4Jb4WM9rMNUfk5F+LnqfW5rdkTFr2oKIqWjc z5fh8DAlJKtUo4WeJWyF1S3Q0+lyRSkUH8tQPr3Qg7ctbvwf+2j/5qToNWIkzjw5MwL/ ZLx3U1HHV5wDuIm3kJSpADSax3VpN+vtstpORoKg0x2rZsFoA0mU74VKeLZsv8CWfbyI gpTg== 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=pnogRv6P2EdhZlVXH4Z31eC8bqrWUx0N9Dr5suFDyHA=; b=deRnWNYXsaw4AOOfoVcqdhx+fA4B+defczIYCp3tfB55E1Bk9+87o6ySeQdOqHtTnf dBGl8oDlQtAnB51jHR1uxSfnuFDkwZ8fR1xVwOfidr9+AuY9Srt1m6XbbHFWLBA5Cd8P YtiXbQwd/qiNYfLTbMeSfItaYNT1hcnTsbToOWtGx08umFTwR6UNikNiffu1IeNx1PH7 RNcJO9lFStnFbpJJPiGUdRxPWrQEujuHDq4mfK/uhFfVcf4m21KCESnmlETYDWGyuzA1 KVWw33vrIbWCAJHKryzYTTnaJqp4PiQ4ndcJREqW/R13ycTS7UlE2ACdTyo9xRGB3Rvx TjJQ== 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=pnogRv6P2EdhZlVXH4Z31eC8bqrWUx0N9Dr5suFDyHA=; b=NeXxyMcPebZ+pa8NJtn7QwnCFIgQD7qdT/I+GZq19moqWZXw3u2TR20U+3/Bc8fb+D xs1VCNt46kDgfWPiOesSJhC3usJ5h4bTibEMAsg09yur5eizvjZvskOk0UbdmIJkCvLu 5dtGQA3GxMNgcICMVvc1R6SWOz0C2zZx2pdBdCcpUUPnRdIvEpYkRwYizmfLAkX+BiFb R4hYLE3KHeZX5cX1y1riEfiXOdc9brkZK4NA0ZUJtg4hzOrSsIAOGvjECdxR2x93PL2P ITf0xxtZcDT3Qk1mBMPoF7itX6ftjc+EAJp+xeX88I9Khka3N7/h/8Ez7DJLD+0ZinvR G2EQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAV0GYI87L054R++W+q4WJhdTpiGeOWM2SBFE+M1/u9Um2qQMhfU WWoGEuwK+n4LvIivQXc94Zg= X-Google-Smtp-Source: APXvYqwq0S+hNTUa6CzIP/xow/KhyvUIx9E4p4aJ9CPUQ257llPLQyio32g6mPp18txWBGFfOEckBw== X-Received: by 2002:aca:3906:: with SMTP id g6mr5555061oia.149.1551975409898; Thu, 07 Mar 2019 08:16:49 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:3de5:: with SMTP id l92ls1998032otc.0.gmail; Thu, 07 Mar 2019 08:16:49 -0800 (PST) X-Received: by 2002:a9d:6348:: with SMTP id y8mr8302097otk.287.1551975408680; Thu, 07 Mar 2019 08:16:48 -0800 (PST) Date: Thu, 7 Mar 2019 08:16:47 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <30ae0dc4-cef2-46ad-a280-bdf617a0db4e@googlegroups.com> In-Reply-To: References: <0f5b8d0e-9f1d-47a7-9d39-a9112afb77ea@googlegroups.com> <12cd6b73-7ca6-481c-9503-250af28b8113@googlegroups.com> Subject: Re: [HoTT] Propositional Truncation MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_882_807722760.1551975408083" 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_882_807722760.1551975408083 Content-Type: multipart/alternative; boundary="----=_Part_883_1409335234.1551975408083" ------=_Part_883_1409335234.1551975408083 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 theory.= =20 This follows from Simon's canonicity result (at least for X=3Dnatural=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 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 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 > > -Dan=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= =20 > what Nicolai said.=20 > >=20 > > Moreover, in the HoTT book, it is shown that if || X||->X holds for all= =20 > 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 a= ny=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 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. 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 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=20 > 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, send= =20 > 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_883_1409335234.1551975408083 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 fr= om 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. This says that exis= ts 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.=C2=A0

Martin

On Thu= rsday, 7 March 2019 14:10:56 UTC, dlicata wrote:
Just in case anyone reading this thread later is confuse= d about a more beginner point than the ones Nicolai and Martin made, one po= ssible stumbling 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 i= s inhabited. =C2=A0For example, in cubical models with canonicity, it is tr= ue that a closed term of type ||A|| evaluates to a value that has as a subt= erm a closed term of type A (the other values of ||A|| are some =E2=80=9Cfo= rmal compositions=E2=80=9D of values of ||A||, but there has to be an |a| i= n there at the base case). =C2=A0This is consistent with what Martin and Ni= colai 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;es= cardo...@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+unsubscribe@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@googlegroups.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_883_1409335234.1551975408083-- ------=_Part_882_807722760.1551975408083--