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, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pf1-x43d.google.com (mail-pf1-x43d.google.com [IPv6:2607:f8b0:4864:20::43d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 33177bd2 for ; Fri, 3 May 2019 11:45:33 +0000 (UTC) Received: by mail-pf1-x43d.google.com with SMTP id d21sf2938583pfr.3 for ; Fri, 03 May 2019 04:45:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1556883932; cv=pass; d=google.com; s=arc-20160816; b=Svz2T8bhgrwKmCdJhaBWcCNb0A0+gEsQPmsqCSGp6yf1aJJfn2SAUT23QOgRny24XW KkqQFxITETWauzFMM6PMiV5W5f655+SdrvLkLxlb8JeJc3tg0kHjb6FVFPhgacwMHUtk ijuPkrYaeJWImGCly4Cvf+u6J4pf5MVEsYNJIeATNjS0J//DJrfI22VUGs832pQQlpeY 6qB3zvaFKXn86KBSyHlO2xm625Ak3SIbVye57iLe/WPRFBFx98okagKm+2k8Nxr/xJ2P DPZR7no7RNvM/4ec4lX3Txa/jF7O0fBUZOMKvGhr2xyuWzB9rPyOROIC9yT2CM8LqpyQ S+Jg== 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; bh=LkDRKCfongLPHpgohuvtKBzKSyGqnOBuCb4XhWGnqN0=; b=zjqB1Fv92CdQqxwjT0aXnmunictEp3clb5SVZSt8esZFSVD6BFhFRs5Ms+v+QMXx8u mm36UWjRWPyj+632SkWBcq0nwRMtO4pUrsjFtX+s5lwVW0mR8AkrX5yJkc0YyUQdB/7O fmHBOEvI6oAR5WnyHrf+EV6RNEgjupGECgrqBIvSqCfs37YOWVszviic7tA+2PkOhDIi Cly6qoE03CabluzN5JELurN9POyvyNoh3PYadK56/rDRLW+b2seJT7pdxZcNGr6P+LvN n35XYLiguLxwVO5YNy77CrcnSLf9OXDfs5eA82JZ4upM+hZgHJ1UiuH4jQ8b6MG4c5Cj TZfw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=1XmyNiPl; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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=LkDRKCfongLPHpgohuvtKBzKSyGqnOBuCb4XhWGnqN0=; b=TSQM3RpMlTb3VBlWf3UCd6FxsrouZrWjxzuRrM+6CWdrjTWkxLh9piBoRTGGDYgJNT qKAZpTO4V6liz9vEX6E3jCh1I8BYmH4crrM+ynfx4reBxXNYhgQ6ug8F0WKnO5uL/cx2 GXg1+HNiTLmnDJKJAUc2h5PWQ5ONu3DqNRDbiwcCEQnLkMGW/prKdYSaoPzmQiU7zq8a WYgo1F8WPekrdLnjXxvi0UKtgpnPh2ciZur3YETE7Os6IotvU0Dbl0IoQz+SqoTH49s6 JRAkM9+pg/BCQ6A6QD01k4pwWPiS30ZmPkSkODgOPnl4lMWZGZnLaR6/rVO6N+FhIOOQ jgyA== 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=LkDRKCfongLPHpgohuvtKBzKSyGqnOBuCb4XhWGnqN0=; b=n71NlnMvK33StERTsQIxzjoIXxivssCGMMhf0CwapVRKv24buwo0dUvix70RUMLDuV yEcKbPH0RuWSY4Z4ISE/a75XYEFa04LbTs7oG+G7WntzgJDP+fIp/4XXk3Ew62NC6lyx BVLbCnFXdlH7Mzl52ySxUgJoJ/gLlLZGTej+CdNvYN1nIf1m6oGAPzE+fGQNBH1ReNFq UthVMn683+KISDZJMnisYflTOq4JgypRy5Aiu3D/Gkx9EC9R5ZAnHL2PCM2Dx2R4R9zG P2ZMZv1EOoadn/tahA2fKzoz+dFA2K9d54nWLYjdHy4LqZgBLwMP63JP+gP9vPOtExRh xiNw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAW86rqbX/D+f2m85FVfBnFzkto8ISAL9wicNyvb3K3nSHmEu/Xv n7ZPn8FYGE0Z+LlHF948bzw= X-Google-Smtp-Source: APXvYqxw4b08VYvdTGTS43G/JCjOiBD/o024CyvB6bQUmUS5BB3E4OVRT8Y98fYvPYLVkeE/MlxfrQ== X-Received: by 2002:a17:902:e70c:: with SMTP id co12mr9656988plb.339.1556883932350; Fri, 03 May 2019 04:45:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:b60a:: with SMTP id j10ls1389523pff.6.gmail; Fri, 03 May 2019 04:45:31 -0700 (PDT) X-Received: by 2002:a63:6b08:: with SMTP id g8mr9656276pgc.211.1556883931891; Fri, 03 May 2019 04:45:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1556883931; cv=none; d=google.com; s=arc-20160816; b=FFVv4MfLmYzDVtPkKNWFawfnWT5tpgV0TbKyeIt72OTI885a43A3XpIC5NwPMfdSrQ jXm4GxmEBhzGgkLLqon+27bh6hj+4SLVutvyGCEYlgNHXHPwgkpBiapw6o7VeM+Ss9NZ 892OdgIe8jaOt1cFSUrR9aHkN0onblQ1myRSDRueyHg2AKk4VvoXcNgXCrPi/o+m952l TypeqFtvwVwdBGw8IQ0tPJolnpLeZ1XBHl3xIseJcLdM7OSWJMI3CAWVlDLXzSCC/Jur juOLqVsuTGbmk/bnIhQ4jtrMvdwjNOPjp1G49cHMbFG9dZgJF7PszK0g7Pgo9V97OK8K UMIQ== 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=tos2gc4KVWGzorGLP4cQEKbK+50h8Jnr11ddUVx1VL8=; b=LV5nDpltGZn2ieD3AdXAtYJoLIU+uRB7LrnqMZLqZBVBwoe3pkcFb5QtnHvoUwk8Qi fw2qP7q1dl/hVSomIiRSJ3c5QBTtBRC977YyqUYxI0HMpdoyb6UCC/40eKdTee7DbZ46 Of9ZeXYo28TfN7qIOcbJj9blmmWSjvvJvxVAQdWL3Q7zhZ9Xe4EjGbmMbsUcTflT89hh AMc4UVNf0301HNZgr7ZJQyaKN0GTCj5t7gkWsxy2+PoKidjo7pC5NnP0UrWITwrSPOcS oE0GGDDaqrg1G2F7A2kOFW6VtTG9GdByPXzP99l81jt3kMnTnIXUqtvgcqGbNY9l20vW f0EA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=1XmyNiPl; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc36.google.com (mail-yw1-xc36.google.com. [2607:f8b0:4864:20::c36]) by gmr-mx.google.com with ESMTPS id 78si109138pft.1.2019.05.03.04.45.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 03 May 2019 04:45:31 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c36 as permitted sender) client-ip=2607:f8b0:4864:20::c36; Received: by mail-yw1-xc36.google.com with SMTP id x204so4037400ywg.6 for ; Fri, 03 May 2019 04:45:31 -0700 (PDT) X-Received: by 2002:a25:487:: with SMTP id 129mr7117080ybe.232.1556883931345; Fri, 03 May 2019 04:45:31 -0700 (PDT) Received: from mail-yw1-f42.google.com (mail-yw1-f42.google.com. [209.85.161.42]) by smtp.gmail.com with ESMTPSA id w189sm604688ywe.42.2019.05.03.04.45.30 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Fri, 03 May 2019 04:45:30 -0700 (PDT) Received: by mail-yw1-f42.google.com with SMTP id x204so4038216ywg.6 for ; Fri, 03 May 2019 04:45:30 -0700 (PDT) X-Received: by 2002:a0d:cb84:: with SMTP id n126mr7348013ywd.154.1556883930179; Fri, 03 May 2019 04:45:30 -0700 (PDT) MIME-Version: 1.0 References: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com> <7104f60a-7dba-4574-8629-860c0bc31967@googlegroups.com> <2b380e43-8623-4900-b529-1e267155562f@googlegroups.com> In-Reply-To: <2b380e43-8623-4900-b529-1e267155562f@googlegroups.com> From: Michael Shulman Date: Fri, 3 May 2019 04:45:18 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Injective types To: Martin Hotzel Escardo Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=1XmyNiPl; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c36 as permitted sender) smtp.mailfrom=shulman@sandiego.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: , 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 formu= lating universe assumptions in each single definition and theorem is unfami= liar in mathematical practice, and so "typical ambiguity" (pretending there= is only one universe) is potentially a good idea for many (or even most) e= xamples. But not in the paper I advertised in this thread. > > Here I post an example when Giraud did precisely that, namely to assume t= wo arbitrary universes U and V, explaining why this is needed in that level= of generality after the formulation of a theorem and its proof, given to m= e 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). The= n >> 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 repeate= d blank lines removed in this counting of the number of lines) that not onc= e did I need to embed a universe into a larger universe, except when I want= ed to state the theorem that any universe is a retract of any larger univer= se if one assumes the propositional resizing axiom (any proposition in a un= iverse U has an equivalent copy in any universe V). So I would say that suc= h 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 regardin= g universe handling. (And I fear that such a system would potentially multi= ply 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= 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.