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,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x23c.google.com (mail-oi1-x23c.google.com [IPv6:2607:f8b0:4864:20::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ff9a8c36 for ; Thu, 2 May 2019 20:46:25 +0000 (UTC) Received: by mail-oi1-x23c.google.com with SMTP id m207sf1773074oig.4 for ; Thu, 02 May 2019 13:46:25 -0700 (PDT) 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=ssg2fDDsGFawh7fKPOex5hrt92tbsAFhP3vvBb/jkDU=; b=GFN3+g6EmL2AhdXXNbJRGwMZX8R4jFusUnybSNHQkqajFPqtB0pPegqEr7N/3dZgyp xGN2KMHEULn5fBfVCL69bczlDJp4UExjZ2Njnnh5qQoeV8M5vVptsDC8kaJ3Z+5PBXg2 WxNXNEdd61a0ptv62XpO1o1z0WVOdiOhYD2XmF4La+2iOUPUgDPflOoHnTwhm46t6T9m LBOljSoIAMJkGtxW17K9svfEx6ikrDEWYwGwkfHmkA38dSPH0Ds2/wYldJT/swOHjiSL TFFhJulFb0qjiIK1moO3BZh3g85GIzh4mDa+3YZgIG2uIThwzAz6hAPwL7/7RrTSfTMq yZAQ== 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=ssg2fDDsGFawh7fKPOex5hrt92tbsAFhP3vvBb/jkDU=; b=jYthHEDfX+/UuJmeIEukJKQQlRDyjyaWbJZjjdbq6TheFnwn2ujWCgCWBTyfWjrr3I 21sM/w0PqWB6TV2Mgd9sKJntE0r7CDevpuXxt21RhdEH/c4n1eXgWwNgVz1SjWCzg5B0 lXdg7BtV0y37VTKvwoSMPOsePIA5X0Nnm4fYtRqAYNKpfNRprYJ93PAcldB1E8eChNRo 1OBfNyEdFw6OFV66YUVtkyMMQAqZfgKhnEyQ9wD2m9804wZzKe8GB9Z9Ku9KRQS2yTod /uqWnFWsHd9GcV+3Z8J8fxBcRTwgYEw4QGyp6Jk6qb3G0P410RdShY82mSXBYR5f/v93 OvQQ== 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=ssg2fDDsGFawh7fKPOex5hrt92tbsAFhP3vvBb/jkDU=; b=ii4mfhxzBGmwE19XB1F9GwUVheSuqgeZMPv27iWm3dI3ms0L50q3sITLvOXlK/cYGD huRkp1tQ+CwpvkXVTA6eARM4gV0xfsGmgUEqEtpLB4XIdmgypwOJ7QbwKNDX6cgUqfcL GUH7dcXz6Fhk/lKtbr33nwI0uf5Iwlv3VFTJrmk/1bRqZy8Ud1yZxyoCiJ+pzIFVNFoz UO0Or4eoqBwFWLk3h60ztQyq93miFLxhcaCmIQqsO7JxoVOvilMDDlu9fMUAYFgdnzJb K+4wz8PL1LZ/kBHUS6YmfBpKATUG+38dwOfBYOMSETPDkvJyu+3jro8Jv2sqv5zLrM6a /t/g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVIHT2WML7g6Iv08y7azdM3wm/yTuQugk/y8icDliDBesp/LblP VXNfjtYoFipOVjD4H8YzCUo= X-Google-Smtp-Source: APXvYqycuWxAdhYhSHmk+WJJ/abgnKHlHErjHxMNXHAkXmJEMerAIkQ7DDghC2+1eyG6MqgGui8U7Q== X-Received: by 2002:aca:ba54:: with SMTP id k81mr3825500oif.32.1556829983734; Thu, 02 May 2019 13:46:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:b588:: with SMTP id e130ls382102oif.4.gmail; Thu, 02 May 2019 13:46:23 -0700 (PDT) X-Received: by 2002:aca:ecc8:: with SMTP id k191mr3911291oih.103.1556829982985; Thu, 02 May 2019 13:46:22 -0700 (PDT) Date: Thu, 2 May 2019 13:46:22 -0700 (PDT) From: escardo.martin@gmail.com To: Homotopy Type Theory Message-Id: <2b380e43-8623-4900-b529-1e267155562f@googlegroups.com> In-Reply-To: References: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com> <7104f60a-7dba-4574-8629-860c0bc31967@googlegroups.com> Subject: Re: [HoTT] Injective types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_691_1498981178.1556829982346" 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_691_1498981178.1556829982346 Content-Type: multipart/alternative; boundary="----=_Part_692_945864103.1556829982346" ------=_Part_692_945864103.1556829982346 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=20 > Russell universes over Coq-style cumulative Russell universes.=20 > > But isn't there a middle ground with Tarski universes? =20 It would be nice to have such a middle ground, particularly because=20 formulating universe assumptions in each single definition and theorem is= =20 unfamiliar in mathematical practice, and so "typical ambiguity" (pretending= =20 there is only one universe) is potentially a good idea for many (or even=20 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= =20 arbitrary universes U and V, explaining why this is needed in that level of= =20 generality after the formulation of a theorem and its proof, given to me by= =20 Thierry Coquand: https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (photo of one page of= =20 a book). =20 The book is =E2=80=9CCohmologie non abelienne=E2=80=9D (1971,=20 https://www.springer.com/gp/book/9783540053071). Suppose we=20 > have explicit lifting operators Lift : U_i -> U_{i+1}, so that as in=20 > Agda we have unique small polymorphic level assignments. But then=20 > suppose we have *definitional* equalities El(Lift(A)) =3D=3D El(A). Then= =20 > on the (rare) occasions when we do have to explicitly lift types from=20 > one universe to another,=20 I can confirm from a 26k line Agda development (with comments and repeated= =20 blank lines removed in this counting of the number of lines) that not once= =20 did I need to embed a universe into a larger universe, except when I wanted= =20 to state the theorem that any universe is a retract of any larger universe= =20 if one assumes the propositional resizing axiom (any proposition in a=20 universe U has an equivalent copy in any universe V). So I would say that= =20 such situations are *extremely rare* in practice. =20 > we would get stronger cumulativity behavior.=20 > (And I could imagine a proof assistant that implements this and sugars=20 > away the El to look like Russell universes to the user.) =20 At the moment we can choose cumulativity (Coq) or non-cumulativity (Agda),= =20 and there is no system that combines the virtues of Coq and Agda regarding= =20 universe handling. (And I fear that such a system would potentially=20 multiply the vices of both. :-) ) M. --=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_692_945864103.1556829982346 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Wednesday, 1 May 2019 17:55:50 UTC+1, Michael S= hulman 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? =C2=A0

It would be nice to have such a middle ground, p= articularly because formulating universe assumptions in each single definit= ion and theorem is unfamiliar in mathematical practice, and so "typica= l ambiguity" (pretending there is only one universe) is potentially a = good idea for many (or even most) examples. But not in the paper I advertis= ed in this thread.

Here I post an example when Gir= aud did precisely that, namely to assume two arbitrary universes U and V, e= xplaining why this is needed in that level of generality after the formulat= ion of a theorem and its proof, given to me by Thierry Coquand:
<= br>
=C2=A0 https://www.cs.bham.ac.uk/~mhe/giraud-universes.pdf (p= hoto of one page of a book).
=C2=A0
The=C2=A0book is =E2=80=9CCohmologie non abelienne=E2=80= =9D (1971,=C2=A0https://www.sp= ringer.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. =C2=A0But then
suppose we have *definitional* equalities El(Lift(A)) =3D=3D El(A). =C2= =A0Then
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 r= emoved 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 assum= es the propositional resizing axiom (any proposition in a universe U has an= equivalent copy in any universe V). So I would say that such situations ar= e *extremely rare* in practice.
=C2=A0
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.)
=C2=A0
At the moment we can choose cumulativity (Coq) or n= on-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 w= ould potentially multiply 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 http= s://groups.google.com/d/optout.
------=_Part_692_945864103.1556829982346-- ------=_Part_691_1498981178.1556829982346--