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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x239.google.com (mail-oi1-x239.google.com [IPv6:2607:f8b0:4864:20::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 71f252c8 for ; Fri, 8 Mar 2019 14:59:51 +0000 (UTC) Received: by mail-oi1-x239.google.com with SMTP id n205sf4690577oif.18 for ; Fri, 08 Mar 2019 06:59:51 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1552057190; cv=pass; d=google.com; s=arc-20160816; b=N1NiQbZqg59PwLkv4CfRWBeFOXrlU+6CSrn4Z+HtAG/VC7+nGU6Gcj6s0E5doYRUuh qIzgcQC/lAk3ih2hu/xEjWXEXCt3rtxKRW+bQCRvgFH5aKw2f76x/EihyBwUB6gcBu7u qXFQEgM8rZmh51y0hxXEBaVBmCgVIaDBL4AbVcBJQH89exGbeAe5HZn6hToKcTbaAt6A TqVdok+c3cwhY/Rtk6Pmjyq99Oxsk2gJJyG8oZ+vy65whgrEgTgJ2pwqhT8/JTE0iGL/ jGb4aR+RHlJefx9zTt8xz5qhM9OZPbLx1L+90zpN+1rIH61Fvlw3k8rtAx5D/53xnKJ3 Wa5w== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature:dkim-signature; bh=OYQ+s0fLSwW+4e09ZeWb845Y5bAvPkbpGK/SP3WU/DE=; b=rUFqGgOuuneknQ+/zuPqKdAlqMrIXGK7o4Vw5oS4Ha1YK8dJUtd8u8KP194eDU7pze HRyvDiU9tvLOD9sdVa8dkK8jZCwj2ymVs3kXQHWc+R+usdVUFBQT3hTwWo4/rtmg9CuN SWPkrlaAt4bRyjRDSugcHy1V9QtiTDuey6hACEAyXPjLCvjg8Mo1pM03cU8V3kM6NDEo Xs/O1pG5RbtrJb3Icis8VcU7gsbwll1sLjwLTzEjUQ5Ff19ooXxLf2gCSe1Ulw9QBrxl ZtsOUAlUHu4YlRu2ix7UYw+XMGN/0IFmJn8pz6cs5tqKqsWkZxZFY2G5F6RDQ3gpqIW5 L7aw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Uw0wftb4; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::32d as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=OYQ+s0fLSwW+4e09ZeWb845Y5bAvPkbpGK/SP3WU/DE=; b=WpoMD3Z3rwfDedQujHHMK323eSpZJUfl1fNb6kcCB8MJx1NmG0gaXAZGf2/vzP4O2L y62D99L015YbL4AYLE2hMAyiqobVbB7h5jgZ98HasHRgEBkmzSV4Zb7oMzRj+juS3zHx pTMjuovsD5c7SZ8qTSqx/d4rE3diNYK5/SkzCP0beRyaA8P4FrWy+QYWgMEs71fr2xQw Lm49p4OYef/xIAccKBQVLMn7gQWz7ZC2UJeoxesPr8/zX0QYtkgkhgjokRW5S/wX9b6p 6tHsiZ3iOPLC+2IuIbsUbGV+uC/jczm3IpW6XWdDTSqFdb+eNrM18aDrd9X4vd0kxNPB TEgA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=OYQ+s0fLSwW+4e09ZeWb845Y5bAvPkbpGK/SP3WU/DE=; b=h5Imz/ScsYo2ta+nN3Wf7bHMKIItUYdOuzB/J/G3JjXtZ0eDbWS4CUeaFUMjO7g193 bFHsktwk+zVFry9oh1/omvipiOCzChNJsOYwZu6HhmXmuW5mBQHVqjLeoEP4bepE4dTE rOlrYLnJ8lJVpMvpPnzjVxqX88z0kXUcdQzFHWrfoWUfyJM0vZWy3lgbxUcCHXdFLPof ncn1lM3F91twDcdUAJDtzCMXae4Ht6KoAneF+FYGmQIXsaAgBK5UiPWzSpEenHQN4mgv FLYrpGZAqbQ+HwumYXi4x8HWjz+flZPxm80gDtyqmdW7K9X1f+n9YrF9HtpAOiw9cebs MalA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :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=OYQ+s0fLSwW+4e09ZeWb845Y5bAvPkbpGK/SP3WU/DE=; b=Fa9OcQaTsr7MPuEgtESjnuuweK2CrQ886cPvgVFKaAhgK6JNsKVM4/FqtlxAZP+9+P oSmfYCfEEF0gPh6uqKErgaFKt1TKUIcamFAtgdgHZxpCyEXynI23ZTjWc/Sqe4lqhtFc a/fM7z+hIoT5/7NJbDRK2cBxtkDDcylLngoRnCSeR3xeoxA7tABk1O2ygAFVXMT1QIYb VojHENJDgs6IZ0w4v2wJdu+lz1RXHnMvgNeibTU/3bGmox2o5uedhlhXhebPe+8jK8A/ FeIK45tPqOPXpa0e7h9Na+8LK/zi57vnOjc0YdmU4T/n9Bf3nDYp7rWDCxvmyoXn+/ns wlhg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX0JIhN9Uj4AqNFdQL/tHAPEDJSCYgIje8NdtS19folklcA+DfA MlL0dHxcfmR5xpC8xSNtbrw= X-Google-Smtp-Source: APXvYqwEMPtXbp/IzpIGmb0T9hmaMErUakpZfHly5dFmRGn1fS76YuXarddiYzGr5dsn52HwuIzu1g== X-Received: by 2002:a9d:7cd3:: with SMTP id r19mr12224410otn.139.1552057189813; Fri, 08 Mar 2019 06:59:49 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:5c05:: with SMTP id o5ls3302781otk.6.gmail; Fri, 08 Mar 2019 06:59:49 -0800 (PST) X-Received: by 2002:a9d:6d14:: with SMTP id o20mr10562237otp.23.1552057189424; Fri, 08 Mar 2019 06:59:49 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1552057189; cv=none; d=google.com; s=arc-20160816; b=sLDmum0w5tMCCu0et0O4FYIkUVjLVcDU4p9YMZbMPLr4gFeUjJBUXuPonQxcYRvrSJ s7pRXkzP94vMWwUwIPzMwFnmC3W1RX5r4A/IZKmr9J+78qqY6PAkWEpBhgdMAi9lpt5I PatD9j7oO/d4JxfAmu6hDCLTBZbxQ4mQY46U0jwKkBmJi+/h0/WCUfkLlM6yOKyFa5dQ Rty6gEoRYvqFlHnyAEpc/Oblbqtb2CHtGM+oBOoxYYJhJWNyiZm+yBjjaXYcic+OyFHS C/opI1ZIF3U2k7jdCCxX3Zd/hKiSgqxMEbIpk5TM0+oiYIZ4DxxBUGbAVPKetFi8d4F8 fWVw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=QXsGl4l/Mpc19tcsVCxWdXrkY8qN0X3kDDU5Miqv1LY=; b=0xUdnMd+scQLBKjQZDZp4F4RsNGDB9Q0ZxL5A0F/7dkkrqz25ZYRUsEjcNW/BG04kp RFyt3oGtpTwKe319IgOVsnTDCQCZgmhbn/hInN/WUfjg/sfDIC3hk/JT4QqmIqKMIq/y /n6rkm2XamXwsmK2mY/lKuEotSrYh7D02v5VhsKSS16YFh9nhSEy/np+1Yph85Jdyzew zi6Whhr8WKekg8eZ9csUO/BjAmdTr0QZpq4iDeiGSZq/BEuB7dQ2MCbGxrna8TvCkNBd NEbdG0p5TGLdlJr5r2XcEHzYUTbwiR+FGhRlwguPgZEfZiQoBXBGwDxgpRTsZM5r7twn vMbg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Uw0wftb4; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::32d as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ot1-x32d.google.com (mail-ot1-x32d.google.com. [2607:f8b0:4864:20::32d]) by gmr-mx.google.com with ESMTPS id p8si418819oig.5.2019.03.08.06.59.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 08 Mar 2019 06:59:49 -0800 (PST) Received-SPF: pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::32d as permitted sender) client-ip=2607:f8b0:4864:20::32d; Received: by mail-ot1-x32d.google.com with SMTP id n71so17558340ota.10 for ; Fri, 08 Mar 2019 06:59:49 -0800 (PST) X-Received: by 2002:a05:6830:1d8:: with SMTP id r24mr11444308ota.264.1552057188644; Fri, 08 Mar 2019 06:59:48 -0800 (PST) MIME-Version: 1.0 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> In-Reply-To: <7a7c3e3f-df35-42ea-9d89-f0d20b855e9e@googlegroups.com> From: Anders Mortberg Date: Fri, 8 Mar 2019 09:59:36 -0500 Message-ID: Subject: Re: [HoTT] Propositional Truncation To: Homotopy Type Theory Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Dan Licata Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: andersmortberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Uw0wftb4; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::32d as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , In fact, in Cubical Agda you will not get these hcomp's with empty systems. The reason is that because of the way hcomp works in Agda there is a very nice trick to implement the "generalized hcomp" operation of the paper that Dan linked to. I summarized the trick in: https://github.com/agda/agda/issues/3415 I added this to Agda some month ago and it should be possible to update Simon's canonicity proof to get a stronger result saying that the only elements of HITs in the empty context are point constructors (like in the AFH paper). For this to work you also have to impose a "validity" constraint (Def 12 in the ccctt paper Dan linked to) so that empty systems cannot result from substitutions. This is currently not done in Cubical Agda, but if you start with a term with only valid systems then you should never get an empty system. So the extraction of witnesses from existence statements should work as Mart=C3=ADn said in Cubical Agda. -- Anders On Thu, Mar 7, 2019 at 6:23 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > > And this is a wildly speculative question. If we used Andrew Swan's ident= ity type derived from the cubical path type only, as in the abstract librar= y file https://github.com/agda/cubical/blob/master/Cubical/Core/HoTT-UF.agd= a) would we still get this phenomenon? Maybe not? What I mean is that we us= e normal Agda, together with what is offered in that file 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=B6tzel Escard=C3= =B3 wrote: >> >> Oh, this is annoying, because it seems to mean that we would need unboun= ded 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 normalizing is in the empty inte= rval context, and the cubical type theory has =E2=80=9Cempty system regular= ity=E2=80=9D (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf). >>> >>> 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. In HITs, Kan composition is treated as = a constructor of the type, and though there are no interesting lines to com= pose in the empty interval context, the uninteresting compositions don=E2= =80=99t vanish in all flavors of cubical type theory. >>> >>> > On Mar 7, 2019, at 5:41 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: >>> > >>> > So I presume that when we ask cubical Agda to normalize a term of typ= e || Sigma (x:X), A x || we will get a term of the form |x,a| and so we wil= l see the x in normal form, where |-| is the map into the truncation, 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: >>> > >>> > https://arxiv.org/abs/1607.04156 >>> > >>> > 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 ca= n compute a witness to an existence. So if in context G =3D i_1 : II, ..., = i_n : II (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=B6t= zel Escard=C3=B3 wrote: >>> > I got confused now. :-) >>> > >>> > Seriously now, what you say seems related to the fact that from a pro= of |- t : || X || in the empty context, you get |- x : X in cubical type th= eory. This follows from Simon's canonicity result (at least for X=3Dnatural= numbers), and is like the so-called "existence property" in the internal l= anguage 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 th= at exists in the empty context behaves like Sigma. But only in the empty co= ntext, because otherwise it behaves like "local existence" as in Kripke-Joy= al semantics. >>> > >>> > Martin >>> > >>> > On Thursday, 7 March 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 closed t= erm 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 ba= se 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 sens= e) doesn=E2=80=99t necessarily mean there is a map A -> B internally. >>> > >>> > -Dan >>> > >>> > > On Mar 5, 2019, at 6:07 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: >>> > > >>> > > Or you can read the paper https://lmcs.episciences.org/3217/ regard= ing what Nicolai said. >>> > > >>> > > 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 in= variant under equivalence.) >>> > > >>> > > The above paper shows that unrestricted ||X||->X it gives excluded = middle. >>> > > >>> > > However, for a lot of kinds of types one can show that ||X||->X doe= s hold. For example, if they have a constant endo-function. Moreover, for a= ny type X, the availability of ||X||->X is logically equivalent to the avai= lability of a constant map X->X (before we know whether X has a point or no= t, in which case the availability of a constant endo-map is trivial). >>> > > >>> > > Martin >>> > > >>> > > 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. S= ee the exercises 3.11 and 3.12! >>> > > -- Nicolai >>> > > >>> > > On 05/03/19 22:31, Jean Joseph wrote: >>> > >> Hi, >>> > >> >>> > >> From the HoTT book, the truncation of any type A has two construct= ors: >>> > >> >>> > >> 1) for any a : A, there is |a| : ||A|| >>> > >> 2) for any x,y : ||A||, x =3D y. >>> > >> >>> > >> 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? >>> > >> -- >>> > >> 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. >>> > > >>> > > >>> > > -- >>> > > 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, s= end an email 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 Gr= oups "Homotopy Type Theory" group. >>> > To unsubscribe from this group and stop receiving emails from it, sen= d an email 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= "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.