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-ed1-x53d.google.com (mail-ed1-x53d.google.com [IPv6:2a00:1450:4864:20::53d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c226c181 for ; Fri, 3 May 2019 18:23:50 +0000 (UTC) Received: by mail-ed1-x53d.google.com with SMTP id n23sf4547632edv.9 for ; Fri, 03 May 2019 11:23:50 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1556907830; cv=pass; d=google.com; s=arc-20160816; b=uwzILWehQ53CCjpHDZKla4oUgUjAT5pT9GrKZpFY9yjFmxIHS1U8dBDZP9boTkRPZH C7pLcOx9PyF7qASop20IIg3INVUUal2Dz/luxHsowSQwyeuc86omcCy5628eqzr0auJM 1fowkdh0IJqD4Wq5hBNCOQ4iYGB6YTKRCFZNHD3NAdOPVixtsytVvfLnpDzuTbRCsDk2 ghNEuwJjE+Se0nsGLmPeLvEzRqKlceN5AKYMBeTwI9mIf3+GU5GxwwTYQdZMxJfHLf1I iI46li3e8rpNYLPQgEqfLbl76TU5aEHyspKAvfQvNm7uSkqFACC6rIwQ9iQEQP3sG1uH VcRg== 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:mime-version:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:sender:dkim-signature; bh=igcPW8VwZi0hYQu/ecjVvPg1PDw8PjjiDkWoZVOakig=; b=UOVi9lwBx1hoonmUvrYQUYWyU5pyrEan7Le+D0uc48uRYcH28RI6pciTLkdEf2GVif KRFUHPDsZPDWPTDGv9n4oVUQkm8TXqXYNe4N6UsOtpUZ4ASDaTwBOOuyI+Lhjl5i+Jdp mA6brQb9lzMuj/4z6LuuZQEVEWf+mkjt/czdvM5y14wYwnnfEMv4JcGUT6ebo3YWkgxB tAuC8EOzdO6EwosmatR30TrEfsgjEmRuYA3RfTX2VZwpyL0GbVa2rLkMhXKmi2D/NUA9 pbHuR81D2S+IHPG91MOeLDCtNegC9ZdEP5s06+RZ95x4viqffAosxmSHVU+OhPhUJ3L0 WJhg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thierry.coquand@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=Thierry.Coquand@cse.gu.se DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=igcPW8VwZi0hYQu/ecjVvPg1PDw8PjjiDkWoZVOakig=; b=AoeG/0brH/tw8yCq1lgDnnmGMUCGdUyYWei2RxZRISU/gfkdp00lVLcEjdA1nIRn9v uJdf2dYdLNSZjodQASQuWMYM7TDWs0Cu/Av7MKPu9KM+M16i9ezfDThpqdQFlxoUxyQJ fyIaJXi1BdSeLHXZzkli0MJnu6P+oqzCtIv20rqsUUQq79pCGt9ulizN07SpkAquU51V 9NnpbCxLblSbY/ppKBuwq3Zllge4VEVeKshFtxbum1MOuovqpfb38rct5e+TjrH9Fi2T DfDZceVhuuxe3cAQ3TyfYKKcBFRj8n2f7Wl/scBObvqJ5WVjThMy/YqnSFS8M+NuZ9qT BbNQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:mime-version: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=igcPW8VwZi0hYQu/ecjVvPg1PDw8PjjiDkWoZVOakig=; b=kr8PskEGjCZbBAwfSdSDrwgRftSwyNG3WQj5PZ71TCAKMkfg1HDao1ZDXwiXf/Krky xGfyc5s2Iw/XzPl8kC0v0BY3TAgVqmSBqFukUmhG04W2aHWXqEJJq2lwAuw2pS/w2SEl cSmqDfhEmYpbO78e+mmZSdto3ptNHHZT43UeK5VKn6Z0c8XTL2AYSHAOtIyS3IM3NCnJ CQoKCTGR8bLxwZSryTlwnAOfuA+gdgn8+btj8wmOAqWmo1dGt/anni1JlktFqDtuYXoJ K43Nu9bYe0P0eZ2pPVrEFr2n4pI6ZraBt2/TuX9MPCgHi+QUTkbnbeXQtxHVaV1Tzwmr j4ZQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWk8cbxM4dPNnCPuyG7vZ05uMRUzoHSoS+YUnu8KD/sLKSYxJ+O 6JRHreTNBhSJmgs15CQzYbc= X-Google-Smtp-Source: APXvYqwI1i5j+IbD2/AcqWJFEVAySAxODxDHYgaxBvrK2zpQvKydTH29LGjpUApMMU3q0z6eobDylA== X-Received: by 2002:a50:9987:: with SMTP id m7mr9850567edb.286.1556907830251; Fri, 03 May 2019 11:23:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:bc06:: with SMTP id j6ls1487266edh.8.gmail; Fri, 03 May 2019 11:23:49 -0700 (PDT) X-Received: by 2002:a50:8684:: with SMTP id r4mr10210431eda.98.1556907829713; Fri, 03 May 2019 11:23:49 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1556907829; cv=none; d=google.com; s=arc-20160816; b=CKDkw+Ypz+pPa28/IrhpGPcsfm6rXB6oQC0QKHUCbvnD71zLegWASQubUdcVdYwpId wlqa8kEyHi9KiMhzywPQiF/Ha8JG5EbSjjQ0Z+XYzYNaPDbpI6oqjZ9HKLdwnQo1kpp8 szMnmXE454h3S+WRq7hgHaVnEKHnxCfHhY/HqpBhue5uvkoU0/mZqcl0RuDtJwtWU04N WcnmQ4MEPeQb2V/RsHf62BjZfScZ62PHCSADGTmj3FxsM9ET8iGKKmYr54YOqHSn4cMM t/YqfqDE74/zp4loKDW5B21dnUXzCmyKEDIAQQ72KnTuAIO6hrTV07tUT5h7R82sVZ25 sHYw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:cc:to :from; bh=H2Az2iegnO9d+2FkR8eT/0XplGkonYSNIZ8pD/pBvNM=; b=mhNFIsKVt05DprfmRJPV2OOu6x+a8Y2Ay3mjXAnKlwX3JZyuuTQC62wjrPHXw6PGmP xK1xdmD1EUOPoDpAs1A1RV/wKiv/3VDSi27hG5sKTfyh8pAeqKu7R88LO6w3uj7+7V3m zC5ZVUt+yGMBv1gImDZuwp1LEpk4b8JZQSRN40jVRu8hvbEAd9znO0RYpUkJL5G9azvn 2u5RQjP0Ka9UExAOFIxxg6DfYubmB5VDZdHBZAUSjMai5FibqVGlD+rhPxeO1LFHbXV8 Ek+2zeD3mRKypw21dv7ufdVhr8q5PwmFj6TGjy/CqB7wVN9ci7fPhAhHTYMnssFjAmvs +oHg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thierry.coquand@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=Thierry.Coquand@cse.gu.se Received: from stark.ita.chalmers.se (stark.ita.chalmers.se. [129.16.226.131]) by gmr-mx.google.com with ESMTPS id w5si178086edw.1.2019.05.03.11.23.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Fri, 03 May 2019 11:23:49 -0700 (PDT) Received-SPF: pass (google.com: domain of thierry.coquand@cse.gu.se designates 129.16.226.131 as permitted sender) client-ip=129.16.226.131; Received: from tyrell.ita.chalmers.se (129.16.226.132) by stark.ita.chalmers.se (129.16.226.131) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.1713.5; Fri, 3 May 2019 20:23:49 +0200 Received: from tyrell.ita.chalmers.se ([129.16.226.132]) by tyrell.ita.chalmers.se ([129.16.226.132]) with mapi id 15.01.1713.004; Fri, 3 May 2019 20:23:49 +0200 From: Thierry Coquand To: Kenji Maillard CC: "HomotopyTypeTheory@googlegroups.com" Subject: Re: [HoTT] Injective types Thread-Topic: [HoTT] Injective types Thread-Index: AQHU/6lEO8V6o5TG8keRT0XUwgiUMKZVcIOAgAA7/YCAALALAIAB0s4AgAD7KQCAABwWgIAAU0EA Date: Fri, 3 May 2019 18:23:49 +0000 Message-ID: <61705DD9-1F89-400F-8059-C2CCADE18B39@chalmers.se> References: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com> <7104f60a-7dba-4574-8629-860c0bc31967@googlegroups.com> <2b380e43-8623-4900-b529-1e267155562f@googlegroups.com> <5782d183-f880-9a85-78bf-49c86687473f@gmail.com> In-Reply-To: <5782d183-f880-9a85-78bf-49c86687473f@gmail.com> Accept-Language: en-US, sv-SE Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [129.16.10.245] Content-Type: multipart/alternative; boundary="_000_61705DD91F89400F8059C2CCADE18B39chalmersse_" MIME-Version: 1.0 X-Original-Sender: thierry.coquand@cse.gu.se X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thierry.coquand@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=Thierry.Coquand@cse.gu.se 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: , --_000_61705DD91F89400F8059C2CCADE18B39chalmersse_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Indeed! There is also http://www.math.ias.edu/Voevodsky/files/files-annotated/Dropbox/Unfinished_= papers/Type_systems/UPTS_current/Universe_polymorphic_type_sytem.pdf Thierry On 3 May 2019, at 15:25, Kenji Maillard > wrote: I think the paper "A calculus of constructions with explicit subtyping" by Ali Assaf that can be found at https://hal.inria.fr/hal-01097401 is a relevant reference for coercive lifts between Tarski style universes. K. On 03/05/2019 13:45, Michael Shulman wrote: I am more optimistic: I think there's a good chance we could do better than both Coq and Agda. Of course sometimes when we try new things they flop; but we can't make progress without trying new things. For one thing, I don't think we should conflate typical ambiguity with cumulativity. It just so happens that Coq has both and Agda has neither, but in principle I see no reason they have to go together. I see typical ambiguity as basically syntactic sugar or abuse of notation, analogous to the use of implicit arguments: the reader or proof assistant is tasked (if they feel like it) to go through and insert level parameters as needed, accumulating constraints on these parameters according to how the instance are used and thereby "elaborating" a typically ambiguous development to a fully precise one with (polymorphic) universe levels. Usually this will be possible, but occasionally if the writer was careless there may be a universe inconsistency. It seems to me that this could be done in both a cumulative and a non-cumulative system. True, in a non-cumulative system we get different constraints, e.g. if we ever write "A=3DB" then it must be that A and B live in the same universe, whereas in a cumulative system we could be looser about such constraints. But your evidence (and that of other universe-polymorphic users of Agda) suggests that such constraints arising from non-cumulativity are not in practice a problem. In fact, the unique assignment of levels in a non-cumulative system suggests that the universe inference algorithm in a hypothetical typically-ambiguous non-cumulative proof assistant would probably be *simpler*, and less error-prone, than that of Coq. So I don't see any argument here against typical ambiguity, as long as there is the *option* to be unambiguous when necessary (which again, even Coq now supports). In particular, note that when a development is formalized in a typically ambiguous proof assistant, it's not necessary for the universe levels to be written in the source code, or even thought about by the author, in order for the interested reader -- or even the author themselves! -- to learn about what the universe constraints are. They only have to compile the code, in particular running it through the universe checker/elaborator, and then inspect the resulting universe levels/constraints. I've done this in present-day Coq myself, although the proliferation of universe parameters makes the output hard to undertsand; I expect it would only be easier in a hypothetical typically-ambiguous non-cumulative proof assistant. So it seems to me that it should be possible to be "fair to the reader", as you say, and still retain (some of) the advantages of typical ambiguity. I also think there's a good chance we can retain some cumulativity without losing the benefits of non-cumulativity, by using a Tarski-style lifting coercion as I sketched in my last email. (Isn't this in the literature somewhere? I didn't think I'd made it up.) I agree that it's rare to need this, but neither is it unheard-of; so if we can make it more convenient to use with no drawback, why not? (Of course, cumulativity is also trickier to model semantically, but probably possible.) On Thu, May 2, 2019 at 1:46 PM > wrote: On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote Yes, this is a good point in favor of Agda-style non-cumulative Russell universes over Coq-style cumulative Russell universes. But isn't there a middle ground with Tarski universes? It would be nice to have such a middle ground, particularly because formula= ting universe assumptions in each single definition and theorem is unfamili= ar in mathematical practice, and so "typical ambiguity" (pretending there i= s only one universe) is potentially a good idea for many (or even most) exa= mples. But not in the paper I advertised in this thread. Here I post an example when Giraud did precisely that, namely to assume two= arbitrary universes U and V, explaining why this is needed in that level o= f generality after the formulation of a theorem and its proof, given to me = by Thierry Coquand: https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo of one page of= a book). The book is =E2=80=9CCohmologie non abelienne=E2=80=9D (1971, https://www.s= pringer.com/gp/book/9783540053071). Suppose we have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in Agda we have unique small polymorphic level assignments. But then suppose we have *definitional* equalities El(Lift(A)) =3D=3D El(A). Then on the (rare) occasions when we do have to explicitly lift types from one universe to another, I can confirm from a 26k line Agda development (with comments and repeated = blank lines removed in this counting of the number of lines) that not once = did I need to embed a universe into a larger universe, except when I wanted= to state the theorem that any universe is a retract of any larger universe= if one assumes the propositional resizing axiom (any proposition in a univ= erse U has an equivalent copy in any universe V). So I would say that such = situations are *extremely rare* in practice. we would get stronger cumulativity behavior. (And I could imagine a proof assistant that implements this and sugars away the El to look like Russell universes to the user.) At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda), = and there is no system that combines the virtues of Coq and Agda regarding = universe handling. (And I fear that such a system would potentially multipl= y the vices of both. :-) ) M. -- 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 "= 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. --=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. --_000_61705DD91F89400F8059C2CCADE18B39chalmersse_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable  Indeed!
 There is also  

http://www.math.ias.edu/Voevodsky/files/fi= les-annotated/Dropbox/Unfinished_papers/Type_systems/UPTS_current/Universe_= polymorphic_type_sytem.pdf

 Thierry

On 3 May 2019, at 15:25, Kenji Maillard <chocobodralliam@gmail.com> = wrote:

I think the paper "A calculus of constructions with ex= plicit subtyping"
by Ali Assaf that can be found at https://hal.inria.fr/hal-01097401 is
a relevant reference for coercive lifts between Tarski style universes.

K.

On 03/05/2019 13:45, Michael Shulman wrote:
I am more optimistic: I think there's = a good chance we could do better
than both Coq and Agda.  Of course sometimes when we try new things they flop; but we can't make progress without trying new things.

For one thing, I don't think we should conflate typical ambiguity with
cumulativity.  It just so happens that Coq has both and Agda has
neither, but in principle I see no reason they have to go together.  I=
see typical ambiguity as basically syntactic sugar or abuse of
notation, analogous to the use of implicit arguments: the reader or
proof assistant is tasked (if they feel like it) to go through and
insert level parameters as needed, accumulating constraints on these
parameters according to how the instance are used and thereby
"elaborating" a typically ambiguous development to a fully precis= e one
with (polymorphic) universe levels.  Usually this will be possible, but occasionally if the writer was careless there may be a universe
inconsistency.

It seems to me that this could be done in both a cumulative and a
non-cumulative system.  True, in a non-cumulative system we get
different constraints, e.g. if we ever write "A=3DB" then it must= be
that A and B live in the same universe, whereas in a cumulative system
we could be looser about such constraints.  But your evidence (and
that of other universe-polymorphic users of Agda) suggests that such
constraints arising from non-cumulativity are not in practice a
problem.  In fact, the unique assignment of levels in a non-cumulative=
system suggests that the universe inference algorithm in a
hypothetical typically-ambiguous non-cumulative proof assistant would
probably be *simpler*, and less error-prone, than that of Coq.  So I don't see any argument here against typical ambiguity, as long as
there is the *option* to be unambiguous when necessary (which again,
even Coq now supports).

In particular, note that when a development is formalized in a
typically ambiguous proof assistant, it's not necessary for the
universe levels to be written in the source code, or even thought
about by the author, in order for the interested reader -- or even the
author themselves! -- to learn about what the universe constraints
are.  They only have to compile the code, in particular running it
through the universe checker/elaborator, and then inspect the
resulting universe levels/constraints.  I've done this in present-day<= br class=3D""> Coq myself, although the proliferation of universe parameters makes
the output hard to undertsand; I expect it would only be easier in a
hypothetical typically-ambiguous non-cumulative proof assistant.  So it seems to me that it should be possible to be "fair to the reader&qu= ot;,
as you say, and still retain (some of) the advantages of typical
ambiguity.

I also think there's a good chance we can retain some cumulativity
without losing the benefits of non-cumulativity, by using a
Tarski-style lifting coercion as I sketched in my last email.  (Isn't<= br class=3D""> this in the literature somewhere?  I didn't think I'd made it up.) &nb= sp;I
agree that it's rare to need this, but neither is it unheard-of; so if
we can make it more convenient to use with no drawback, why not?  (Of<= br class=3D""> course, cumulativity is also trickier to model semantically, but
probably possible.)





On Thu, May 2, 2019 at 1:46 PM <escardo.martin@gmail.com> wrote:


On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael Shulman wrote

Yes, this is a good point in favor of Agda-style non-cumulative
Russell universes over Coq-style cumulative Russell universes.

But isn't there a middle ground with Tarski universes?

It would be nice to have such a middle ground, particularly because formula= ting universe assumptions in each single definition and theorem is unfamili= ar in mathematical practice, and so "typical ambiguity" (pretendi= ng there is only one universe) is potentially a good idea for many (or even most) examples. But not in the paper I adver= tised in this thread.

Here I post an example when Giraud did precisely that, namely to assume two= arbitrary universes U and V, explaining why this is needed in that level o= f generality after the formulation of a theorem and its proof, given to me = by Thierry Coquand:

  https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo = of one page of a book).

The book is =E2=80=9CCohmologie non abelienne=E2=80=9D (1971, https://www.springer.com/gp/book/9783540053071).

Suppose we
have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in=
Agda we have unique small polymorphic level assignments.  But then
suppose we have *definitional* equalities El(Lift(A)) =3D=3D El(A).  T= hen
on the (rare) occasions when we do have to explicitly lift types from
one universe to another,

I can confirm from a 26k line Agda development (with comments and repeated = blank lines removed in this counting of the number of lines) that not once = did I need to embed a universe into a larger universe, except when I wanted= to state the theorem that any universe is a retract of any larger universe if one assumes the propositional resiz= ing axiom (any proposition in a universe U has an equivalent copy in any un= iverse V). So I would say that such situations are *extremely rare* in prac= tice.

we would get stronger cumulativity beh= avior.
(And I could imagine a proof assistant that implements this and sugars
away the El to look like Russell universes to the user.)

At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda), = and there is no system that combines the virtues of Coq and Agda regarding = universe handling. (And I fear that such a system would potentially multipl= y the vices of both. :-) )

M.

--
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 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 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.
--_000_61705DD91F89400F8059C2CCADE18B39chalmersse_--