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 8370be5c for ; Wed, 1 May 2019 06:25:33 +0000 (UTC) Received: by mail-oi1-x23c.google.com with SMTP id b14sf5922265oii.3 for ; Tue, 30 Apr 2019 23:25:33 -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=g5FmwJGfs6GUJ8sjlMCl7k10VZIr1zOk5qQKo15v5KI=; b=J1/MtoXxKK6Q3YwqH6sf6iHbHvHFMija0XFQeq740JK3vsU/k9oU2hNhevv9aoLPe9 iW2lursnONLIVSH8fPX5SYZIoWzW7re35LNwjksuf1BJVYyMjNIKJeAJgqzDStxugSNC jBUwhwB1i1upOutnjnUCcu7lFp1flpx87TkTGR3eqL1PsmHamIuowPWX3vwub94LcK76 o0SKMTxfRUUgL4Wge5IDXWjtjjjrGNE9C0ktZnmP2EbuVyI8778FwEdrZ/Wde1pKoAJV h1djRvyuTCo5vPCQIYrk2/XTWEdtuwC9nY10L/V+OWj6u9QgQYBoZt76tbp+CX7sDYTX 4ulw== 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=g5FmwJGfs6GUJ8sjlMCl7k10VZIr1zOk5qQKo15v5KI=; b=qs4yfEBeZxOGIuusfGzwnun6eeOzSb3RrfcDc5eEnt69W2xFzSmG+LEE4JpUqWvpGb Zlo0bs1VJbMmWBw+ik03IQNEeTk2ghhrONWS4M+oGgJVQuOc8/qp3BSshSOQRFUN9wGz XSYYV9+CrSTI4l4SEr0QkfBjLjRWUUylQi8FIzoatDZSB+Z80MgcVTG2YXzlwMKghB/q RGJpvRGptLCjt+KCnRqWezasOyqmpXBdmPrz+TCfQHc0wLy0xtPc7xlqxtbQIdIxPVE7 KXoIVtDAauGQ5FigoY5IVH/lNAV9YwFBF1WdHuJLK/XkDp5BMGA5ktNcuB2jYjGkfvhY Ma6A== 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=g5FmwJGfs6GUJ8sjlMCl7k10VZIr1zOk5qQKo15v5KI=; b=IMGFqxQ0MgBbPUYDt5mHeWBQ3l/rq/iwNJ8rBWCyiqF296CmFqlbQyKnzN2UmmtGYM uCDAtohbiRAtV6WGhqiB7z5NJWXkgobAt3UIjyJiOKBTiusy23m18m1pITxelVgi43wp AjIFJJUnUj+C7rGuVp2MYN782fdDHH9BOs3gmnAJo4mbcgD87igGE/1nYAnwXR33kQAR 0c+x6ekQ4GO6av1XQQCKGrjg9tyco50wKzpL4yl16z9xUd3jVeyEoImlG3nTWHjfFUCD qUWznNHqdMKD7QbGkXL5sdX7MVlkvjXtDu/pBnnpN/GjhLaMWjVuEz5/nbjwU+DX73Ll 1Iog== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAU1t36MGbr/VWBHUtrr9sBr39mzhfgY/VCVtobSEeXxjbh4xRUG eDgFh6pQWJA5hkFARaLUuos= X-Google-Smtp-Source: APXvYqyOP18hnySdR8b7oGzj+OGN9Xs9bnHDSiy2Ixfgwrn/tklw0+S+S+8rLvRfq7huz5bsDPJvig== X-Received: by 2002:a9d:39c5:: with SMTP id y63mr12006328otb.42.1556691932618; Tue, 30 Apr 2019 23:25:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:578c:: with SMTP id q12ls683577oth.11.gmail; Tue, 30 Apr 2019 23:25:32 -0700 (PDT) X-Received: by 2002:a9d:226b:: with SMTP id o98mr17073499ota.20.1556691932000; Tue, 30 Apr 2019 23:25:32 -0700 (PDT) Date: Tue, 30 Apr 2019 23:25:31 -0700 (PDT) From: escardo.martin@gmail.com To: Homotopy Type Theory Message-Id: <7104f60a-7dba-4574-8629-860c0bc31967@googlegroups.com> In-Reply-To: References: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com> Subject: Re: [HoTT] Injective types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1284_1653266971.1556691931412" 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_1284_1653266971.1556691931412 Content-Type: multipart/alternative; boundary="----=_Part_1285_619619370.1556691931413" ------=_Part_1285_619619370.1556691931413 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On 01/05/2019 03:50, Michael Shulman wrote:> Interesting point! I=20 definitely agree that we don't want to be > *forced* to be typically ambiguous; there are times when we need to > explicitly distinguish universes. This was already the case in a few > places in the book, e.g. Lemmas 10.3.21 and 10.3.22. And Coq's > universe polymorphism now also *allows* the user to explicitly specify > universe levels when desired. (On the other hand, it's also nice to > not be forced to label all universes explicitly all the time. But on > the third hard, at least in Coq as it is now, the interaction of > user-specified universes with automatically-deduced ones seems to be > fairly fragile.) Right. > However, it's not clear to me why cumulativity would be a problem. In Agda each type gets a unique universe (or at most one universe) and often (but not always) the system is able to infer them if we write question marks "?" for them (but not always). Cumulativity is not "on the nose" in the sense that from X : U_l you would get X : U_m for m =E2=89=A5 l. Instead, if you need to have (a copy o= f) X in U_m, you need to use an explicit embedding U_l =E2=86=92 U_m. (I only ever used this embedding to show that U_l is a retract of U_m if we assume propositional resizing.) In practice, however, I never needed to use this embedding, as the closure properties for universes work with more than one universe at a time. For instance, if X:U_l and A : X =E2=86=92 U_m, then =CE=A0 X A : U_{max l m}. With this kind of closure property, I haven't encountered the practical need for cumulativity. It is nice, in practice, that universes are uniquely determined. Insted of thousands of level constraints, we have a unique, small, (polymorphic) level assignment. > In fact you wrote in the paper that "We don't assume that the > universes are cumulative... but we also don't assume that they are > not". Which makes it sound as though cumulativity, though not > necessary, wouldn't be a problem if it did hold -- would it? In theory it wouldn't be a problem if it holds. However, if Agda did have cumulativity, it would lose the unique-level assignment property that I use to infer the levels of the results from my given levels of the data. However, in the absence of a concrete proof assistant with the option to enable and disable cumulativity, it is impossible to perform experiments to confirm or reject this conjectural impression. I consider the universe-level system of Agda to be excellent in practice, and easy to use. Moreover, as I said, if I publish a mathematical theorem developed in Agda, I think it is fair to the reader to let them know what the universe level assignments are rather than just say that they exist. In some cases, as injectivity, the universe levels are crucial, and if we ignore them we get false claims. Best, Martin --=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_1285_619619370.1556691931413 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On 01/05/2019 03:50, Michael Shulman wrote:> Inter= esting point!=C2=A0 I definitely agree that we don't want to be
> *forced* to be typically ambiguous; there are times when we need to=
> explicitly distinguish universes.=C2=A0 This was already th= e case in a few
> places in the book, e.g. Lemmas 10.3.21 and = 10.3.22.=C2=A0 And Coq's
> universe polymorphism now also = *allows* the user to explicitly specify
> universe levels when= desired.=C2=A0 (On the other hand, it's also nice to
> no= t be forced to label all universes explicitly all the time.=C2=A0 But on
> the third hard, at least in Coq as it is now, the interaction = of
> user-specified universes with automatically-deduced ones = seems to be
> fairly fragile.)
Right.

=
> However, it's not clear to me why cumulativity would be= a problem.
In Agda each type gets a unique universe (or at most = one universe) and
often (but not always) the system is able to in= fer them if we write
question marks "?" for them (but n= ot always).

Cumulativity is not "on the nose&= quot; in the sense that from X : U_l you
would get X : U_m for m = =E2=89=A5 l. Instead, if you need to have (a copy of)
X in U_m, y= ou need to use an explicit embedding U_l =E2=86=92 U_m. (I only
e= ver used this embedding to show that U_l is a retract of U_m if we
assume propositional resizing.)

In practice, how= ever, I never needed to use this embedding, as the
closure proper= ties for universes work with more than one universe at a
time. Fo= r instance,

=C2=A0 if X:U_l and A : X =E2=86=92 U_= m, then =CE=A0 X A : U_{max l m}.

With this kind o= f closure property, I haven't encountered the
practical need = for cumulativity.

It is nice, in practice, that un= iverses are uniquely
determined. Insted of thousands of level con= straints, we have a
unique, small, (polymorphic) level assignment= .

> In fact you wrote in the paper that "W= e don't assume that the
> universes are cumulative... but = we also don't assume that they are
> not".=C2=A0 Whic= h makes it sound as though cumulativity, though not
> necessar= y, wouldn't be a problem if it did hold -- would it?
In theor= y it wouldn't be a problem if it holds. However, if Agda did
= have cumulativity, it would lose the unique-level assignment property
=
that I use to infer the levels of the results from my given levels of<= /div>
the data. However, in the absence of a concrete proof assistant w= ith
the option to enable and disable cumulativity, it is impossib= le to
perform experiments to confirm or reject this conjectural i= mpression.

I consider the universe-level system of= Agda to be excellent in
practice, and easy to use. Moreover, as = I said, if I publish a
mathematical theorem developed in Agda, I = think it is fair to the
reader to let them know what the universe= level assignments are rather
than just say that they exist. In s= ome cases, as injectivity, the
universe levels are crucial, and i= f we ignore them we get false
claims.

Be= st,
Martin

--
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_1285_619619370.1556691931413-- ------=_Part_1284_1653266971.1556691931412--