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.0 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-wm1-x33d.google.com (mail-wm1-x33d.google.com [IPv6:2a00:1450:4864:20::33d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id bd47c2ed for ; Fri, 3 May 2019 13:24:38 +0000 (UTC) Received: by mail-wm1-x33d.google.com with SMTP id z21sf3611422wmf.9 for ; Fri, 03 May 2019 06:24:38 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1556889878; cv=pass; d=google.com; s=arc-20160816; b=f7jT/yhLOJG7uT0cqek0I6O/jbaZfmw5kxXhjojQMNOSTEsopDZzh75idrH0CUaa95 alYnWJ2k3w35bLP+MpLQZl/JSMghJFQr9o4gTm6zje/OzCjwT2rqnRINx2BPFOswZ1MQ RwYf8VAcIn5I5PCQVMzHWYiEa+OzdLFDt76zxUKGOyBABS8OPwib0SLUGlMVr+ki0HXj x2j8ZMcoFNwIS6c7wVeEJ02Yjw5KXDINhtLYPqzEI70jyhE9rsn4TD0cRj3mhYBi7dS/ OaV4rcWtdzTfw3fNE1dYpprWqxJ228qposOx9PnTWg+woufAWP51kVQohkR0bO0Dfr4Q 5uAQ== 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-language:content-transfer-encoding :in-reply-to:mime-version:user-agent:date:message-id:from:references :to:subject:sender:dkim-signature:dkim-signature; bh=D/aiTVwIb6dWldTW9MRI8Cu4laJjWFIHUJA2f6oLAek=; b=nWG7CbXwldXPkDtoPb/U+MgqRgUGp7mw7viGGnIyKyNZoZuGiJXxbqxiJXXHmeQ4x1 otXeP2aZGYBPT56/fcw+zlNMiTUcSVlPjHTxf1kxiT7jktj/CC/SBxpgqAm2yGchVusC W84UhCxoG9xsO280P5VtCx4hZ16ARxNkDvpkP7wf9U4eCkIZW0nMYU2rfd60JGcYU4Cb cLyFATKGMDa5uF2mOvSdfo73N7IN9Sn497H2XewbilceSh5SfWwsCTRno26PWpPvq6z3 tTAVUqqO5UIUnabC43eZFKanw7T6d8Z3Hg+fFpFXmULQwSKq+V1f2499/FdXp6ww5eKH dtQg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=FxRHIKvr; spf=pass (google.com: domain of chocobodralliam@gmail.com designates 2a00:1450:4864:20::336 as permitted sender) smtp.mailfrom=chocobodralliam@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:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-transfer-encoding:content-language :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=D/aiTVwIb6dWldTW9MRI8Cu4laJjWFIHUJA2f6oLAek=; b=V20jDCF4L3cTjHwKdWNPkarD8Et2g98DsjecIyqgZwgjX6lGKdlgPfXb7YYk1A10S+ 8bvgZgG194XgEcVxixxlhQZrIw+OhG89cdu40gxUcBWVQT+DxbqhGemHmUAgErvr4fC+ gavHtlWb5CsBsa8GyIh6XAQKVy2xTvVXLbv64NNXMiA8nfW6z1iPnzk8wbzvbd2626Zk ugxzF5jUxCNQQ+PtmF7soWPek4hFi1zD0Q8brPZntnKw5e6x9L4i/uKtgAPprfWLXbGI gbrPGJnsAcL6YSKOFJWAK+0czrYkO4adrC6oI3cngUKLgjbx94x4wPw+8d+eHpnFlTFv x9rQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding:content-language :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=D/aiTVwIb6dWldTW9MRI8Cu4laJjWFIHUJA2f6oLAek=; b=LSutw0XBxx8q6npzlew7qyhlPU3C9EA7uuMjLXjPdwg99ck+K3fGdbFhrioiqZh6gq B0WHwnKOQ2KPQlbYczU18cL3Bg+k/tAHP0F+OY6Yit8GnMpJYvDkF3f0luDOUWWhy9v0 kg8VS194tNfpkC3yTOLBrRIdjBQzi2SyZtozz6gYM1K1sEWnD7MbsrFAO3kYDqmbIUzO pr0j4R/Rb/7D/pDvryPNL9pSL0YwUwS+qKzqEPQtV4WWSRRSN/EOHlqmf7unw4MANK0W uEqUkUpeRBZph3THa7TDLiGBrFBpluAdyjJUYYLHR1QftqQXXANI7BZJcqAgdF38P9ju fEvQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-transfer-encoding :content-language: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=D/aiTVwIb6dWldTW9MRI8Cu4laJjWFIHUJA2f6oLAek=; b=pN4uaoEisUebISaLkPvjfn9b4MZkpR6jXGEWBiqZPNf/LfzdFcrKQeCFQ/PownywhO urQBD8PYkb7oB+xb5CQazaEeXL1qsj9S10bra3hcsAtXDoZ8eR9xMSdQFh4/T3jKqEP/ VoJZMB25PtAnEWbiPgocb9SZ7DfQaW3f9a8ZrhxCAxVqlhrc+x2sqBjCNWkk7+t1YN1l e3x3mQ8IurR82eWMaE6ExTFSRuZMFperSCwnlqj0D/Cq+56jcWE0WlizsDRH2hGnn1Na YyGVv4msoE6CC1X/jMsgvF+qREtZcrbGtUycbMTX7FgV2yGW8gA0W0b+ZLYP1J7ZGbgj Dh6Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVyOwXEMP5xC9uVzkr1Ri825v8+mKBVNispuim6Fe2wR7L46sIl vjxUU8+gdpK/9sFc+WrcMDs= X-Google-Smtp-Source: APXvYqxzbNzu9n8oeymQ8ukvzqTXNv7mKjapU9GPmHgZU6CCL6LicWmC+2+MnG4XtFu3E9sHglmcuw== X-Received: by 2002:a5d:4403:: with SMTP id z3mr7336911wrq.186.1556889877899; Fri, 03 May 2019 06:24:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:6a8a:: with SMTP id s10ls1348915wru.12.gmail; Fri, 03 May 2019 06:24:37 -0700 (PDT) X-Received: by 2002:a5d:4805:: with SMTP id l5mr7176794wrq.279.1556889877474; Fri, 03 May 2019 06:24:37 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1556889877; cv=none; d=google.com; s=arc-20160816; b=DzAKVaLM2YEyoktDoNqvYlo2w4Zn5HUNt3/ZFWF3i7OXKdHWYOd9czknnwI/fpxSpV BKsa7pVL51H7sKPF8HHX6iPb+TsviDBcCp/eyxBrbFDXbxl0YpEvXRG6MUWVK2TqZ8Ga kAGVCl6TCCWGZ7ORXxeCo8jlVAdCtjqvKrqHElaOZepfzyPlVel1fLe1DSSAT/SNdibW gfLqDf3Yes5BdKTz7QbFLbjCCAeyY5MMQCzPbqiyzrnSb9TwnHfcu4GXsUX2685X54Xt Ec3Xfu2B4UBG0CmAGgzxUnBLoMtiXaJNZrueoWvUdFAkH/EaEqztGKy2DhqjHkNjssiH a7zA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :dkim-signature; bh=Gig+SfNs76xA48jeyCd+AcuO7b5U7xkN2okRRD3mOqE=; b=XwhBrArR5Vjjmes6s7ODNYVSL33lbTwAm1EZhDveXmtfbWYMU1IqvD1qgYXhg5Ad3k 9QYHdgwh6TP0K3NNwA7SEWCaarrydrx0rWmVGX2xr+N6TKDXT5m0mR0ufuXQsR6oSALd tXYxnPbuqNRtNKSABcMbXqSbO6Wfl8UINzj1BkGmKB768Ff3gBHs8VQjWhTQh+kP1wgf hNR1IahLqOrRfpDv4ho9p7p5xjn4YcjMSgByoWBpDhUtWegXSa8gppb+uBDjHVoztGki nte6e+xWqx7DPJceR3JbGIeOCq9iJD5n5/tRl4C4vNEIfmmYKyy4OMCl1MBqPOIv1r0g lKLQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=FxRHIKvr; spf=pass (google.com: domain of chocobodralliam@gmail.com designates 2a00:1450:4864:20::336 as permitted sender) smtp.mailfrom=chocobodralliam@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x336.google.com (mail-wm1-x336.google.com. [2a00:1450:4864:20::336]) by gmr-mx.google.com with ESMTPS id u2si121804wri.2.2019.05.03.06.24.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 03 May 2019 06:24:37 -0700 (PDT) Received-SPF: pass (google.com: domain of chocobodralliam@gmail.com designates 2a00:1450:4864:20::336 as permitted sender) client-ip=2a00:1450:4864:20::336; Received: by mail-wm1-x336.google.com with SMTP id b10so7117526wmj.4 for ; Fri, 03 May 2019 06:24:37 -0700 (PDT) X-Received: by 2002:a05:600c:2188:: with SMTP id e8mr6536835wme.78.1556889876904; Fri, 03 May 2019 06:24:36 -0700 (PDT) Received: from [128.93.85.240] (wifi-eduroam-85-240.paris.inria.fr. [128.93.85.240]) by smtp.gmail.com with ESMTPSA id s145sm3409244wme.38.2019.05.03.06.24.32 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Fri, 03 May 2019 06:24:35 -0700 (PDT) Subject: Re: [HoTT] Injective types To: HomotopyTypeTheory@googlegroups.com References: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com> <7104f60a-7dba-4574-8629-860c0bc31967@googlegroups.com> <2b380e43-8623-4900-b529-1e267155562f@googlegroups.com> From: Kenji Maillard Message-ID: <5782d183-f880-9a85-78bf-49c86687473f@gmail.com> Date: Fri, 3 May 2019 15:25:49 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Content-Language: en-US-large X-Original-Sender: chocoboDralliam@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=FxRHIKvr; spf=pass (google.com: domain of chocobodralliam@gmail.com designates 2a00:1450:4864:20::336 as permitted sender) smtp.mailfrom=chocobodralliam@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: , 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 form= ulating universe assumptions in each single definition and theorem is unfam= iliar in mathematical practice, and so "typical ambiguity" (pretending ther= e is only one universe) is potentially a good idea for many (or even most) = examples. 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 leve= l of 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 pag= e of a book). >> >> The book is =E2=80=9CCohmologie non abelienne=E2=80=9D (1971, https://ww= w.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). Th= en >>> 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 repeat= ed blank lines removed in this counting of the number of lines) that not on= ce did I need to embed a universe into a larger universe, except when I wan= ted to state the theorem that any universe is a retract of any larger unive= rse if one assumes the propositional resizing axiom (any proposition in a u= niverse U has an equivalent copy in any universe V). So I would say that su= ch 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 regardi= ng universe handling. (And I fear that such a system would potentially mult= iply the vices of both. :-) ) >> >> M. >> >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n 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.