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=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-yw1-xc3d.google.com (mail-yw1-xc3d.google.com [IPv6:2607:f8b0:4864:20::c3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5a93d4ef for ; Wed, 1 May 2019 02:51:07 +0000 (UTC) Received: by mail-yw1-xc3d.google.com with SMTP id c67sf16160405ywb.4 for ; Tue, 30 Apr 2019 19:51:07 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1556679066; cv=pass; d=google.com; s=arc-20160816; b=y+qF7gSzELbox7XZxFXrvj5VYJz1t9CVMWUqIA0hwDtagcletCQC2n9se5+Y2uQi7B TV7tIEAFiMN1QUAqd1YK+eWlRMvAD2/Wt4wq2ShFgeXuZnsgQV6q+/s7GscRNdMhj1J6 QL6WFdUYORVCXjCEaoeaZbdNmX5RU98EUw78xaeHNALVAs9QkKl5k+zEAA4KrGmWSdRD vpLcsw5MylhqQcLw19k/An+c8AQWYlcqMqnV20SqfJoevalZQkp60xIezjhbjZOfmFmg BrKVe/jJOMtfVkYvtX07L3ruBaKwPHf1NKrjkZF/NiQEdXdTZJX83XX5MUN62l1fAO1D aWng== 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=wU9gsTW852HpP7xqK15SowuFq99fGnlmqcbve3yv/kw=; b=B9w5Thpz+GmU0bNuh9ZcfSSEoppXhECL5Wq7cWmu4zkWR6DVqtCK3ktp4/VGUCvUgR xiiXxS+JJsgnWaNUXgIGYHBRJc0wIt53Bd3M++41IPbIJOGKvhDCJwkr3HlwqxWfDqAG itYocjMwOg3v4BjmTUghDHWMT44h4/DlsFbuPefqwFhwC/bUbFIca0JOpNjmOKYiyGyL dfBetTzGO1n4R35NFUDUUtA2IP99ecrSRTsGct5pZ/9aK3Dt1M9FUtJ/CEcXyhUdSGsp IDyVoyI+VvOL77WH3J+WnREIUeyhcGuaWw38sAJFV5yevrZaCAQIluIEzfYWHwqp7voO UkBQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="MKfX/3lq"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2e 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=wU9gsTW852HpP7xqK15SowuFq99fGnlmqcbve3yv/kw=; b=Mlv3OpEtoE97YISu3UPecpkFJc56Kce/QSP/zT0Qb+Za5hoGRXkaiwTAcxl7TnPrBN QWXZckZ54a0VSg7GwG+PX3z+2e2mvjfFvSL4XOc1ObL5/WduDpgzwMtaK2/GkmNiekPC MDVBZuA2417CVJ8Z4Rmwg9LYoN6CJpCi1mdAuljNIBVE46vFMGMdbHJS7DhqkzbidLdI Z6Wu9uTMfvaf5uXZVyXWJzor99QS9w0QxEMq9faCl8W6AlLRB/BIK5TeLN2dzLM79WZ2 +70de6YfVio2pEWY0u9w0dMNLTiV2TT61UILnlpbn/WBonZ2pEr8s9DpETY7DNVPhdU/ +MjQ== 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=wU9gsTW852HpP7xqK15SowuFq99fGnlmqcbve3yv/kw=; b=E4iJvMiIpwpbdKZBytFE0RrNZbUxtFKuiSd61HBUIgUQpyWC5s8i1Ha91/vkHPgwqB MabsUdYT6RhjFMP3zD7p1sJK5VA3cLjl6M2odgKIUSc5hRqlATyjuuYCr/EtO0B8Nr8t 1MiLLqcK0URCcnqE23AqlolpM1z5yw4nR6ovnx1j10RjZN4Fi9ewDLG06Z9EVTG5ErbT jENDUtCJUygV8ca0z6KvL6846VQUExTtgducpEg2n6lK/jySMCKscbit+nKflCZ6LI8u X7aIYECWdC7Xo4OgVT1iWR7NMY1AWrSL4twq4ACn9Prs0ImFyuh4WTiSmiS9gkl5CiFr 5lRg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWfL3jjXbZSxkFDrlPeBg8LlfLGe98yJ+y/1+JoKu/u5U3i3Os9 JY32BLLwVYwvOdNDcg+UDTY= X-Google-Smtp-Source: APXvYqyDGWrMh5dSipAsbOxqr/tJlFwamoHO8lkr5UvxyTX541xwlugeWP2aQ05ICYF7KdChFPG7EA== X-Received: by 2002:a81:4b96:: with SMTP id y144mr48360035ywa.461.1556679066395; Tue, 30 Apr 2019 19:51:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:4a02:: with SMTP id x2ls10625879yba.7.gmail; Tue, 30 Apr 2019 19:51:06 -0700 (PDT) X-Received: by 2002:a25:55c3:: with SMTP id j186mr37802065ybb.255.1556679065969; Tue, 30 Apr 2019 19:51:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1556679065; cv=none; d=google.com; s=arc-20160816; b=H4Vkw+d90iRVws8zNDZ1pgJCgftbx/pC/4njvhXiKiIaj5OJKh45nnnHP1/lV/AU1j t1lEzaOJKcH/Vocog5IE6Nns+rHwRR1f3b0jUSEwplfJunaPgTj6RS/SRfERoF0LHjY+ 7xRKUfTpjsNOnK5QS0rI5flrC+fyJvryu6o6lmm/x5SOQoXRWRIoc8YSnh86/qwoCsGb o9hrcJ+rMhiLoNNNBGrWIgA1h9q+J85q7VcWT2eEgZsBSQ0Mz/5CIpLwW9J1HxJopx18 wq7o8ej+Uux+1XtUZ4nW3eF1n5aKZOX+Pcn0lg7p/iKYJ0tu5b8qY6EPGvPGBKGo+mSr PC7A== 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=Cgjnw2sguEy3qjosT+6pF6fDV008yJqK1K0M9UfjmsE=; b=SLB/OX+KQAs8St1Xm7Ui5GFiYV06Lwm0QasOii4sKK1EA4i8DgiZMu6QP6YrwgPSwq Yki+D9JtsbWIhMpwbNy5pzU0HkROV0lVmtUmEwn3IqdQOaJI09aZoOCOMUeEaX4c8WhQ 0JVQi9700RAVOAeOqujzOdy549iSF1c0qIpzGYeqtKtd2iQNh9aFPL/KPMERrLwng9F+ Wz3a6qjjSYJVZghnFeQ7mlTVStrAuR9j0l2uYKeTK4DUVLyV5YBZtZaWWIfSYLJksF6g JNyCdopeR7eNIBLsHh0gSM+Y5fs0J/bL2CArbE7TXo0Fcey2lrYq9e9GO9sjyzZpA8OM vz2g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="MKfX/3lq"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2e as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc2e.google.com (mail-yw1-xc2e.google.com. [2607:f8b0:4864:20::c2e]) by gmr-mx.google.com with ESMTPS id n194si119984yba.3.2019.04.30.19.51.05 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 30 Apr 2019 19:51:05 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2e as permitted sender) client-ip=2607:f8b0:4864:20::c2e; Received: by mail-yw1-xc2e.google.com with SMTP id v15so7464156ywe.13 for ; Tue, 30 Apr 2019 19:51:05 -0700 (PDT) X-Received: by 2002:a25:4946:: with SMTP id w67mr34756567yba.445.1556679064616; Tue, 30 Apr 2019 19:51:04 -0700 (PDT) Received: from mail-yw1-f44.google.com (mail-yw1-f44.google.com. [209.85.161.44]) by smtp.gmail.com with ESMTPSA id g5sm16573532ywf.100.2019.04.30.19.51.03 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 30 Apr 2019 19:51:03 -0700 (PDT) Received: by mail-yw1-f44.google.com with SMTP id w196so7477081ywd.10 for ; Tue, 30 Apr 2019 19:51:03 -0700 (PDT) X-Received: by 2002:a81:4a46:: with SMTP id x67mr53463518ywa.255.1556679062970; Tue, 30 Apr 2019 19:51:02 -0700 (PDT) MIME-Version: 1.0 References: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com> In-Reply-To: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com> From: Michael Shulman Date: Tue, 30 Apr 2019 19:50:49 -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="MKfX/3lq"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2e 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: , Interesting point! 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. 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.) However, it's not clear to me why cumulativity would be a problem. 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? On Tue, Apr 30, 2019 at 4:05 PM wrote: > > I would like to advertise this paper, which investigates injective types = and algebraically injective types, and their relationship (https://arxiv.or= g/abs/1903.01211). > > In this paper, it is important to take universe levels seriously (for the= reasons explained there). In the HoTT book, and in Coq, the universes are = taken to be cumulative on the nose, and we pretend, notationally, that ther= e is only one universe (this is called typical ambiguity). Based on the exp= erience of this paper, I have the feeling that the loss of cumulativity, as= in Agda, but also as in the infty-topos model of univalent type theory by = Mike (https://arxiv.org/abs/1904.07004) is a good thing. In particular, I a= m not sure how typical ambiguity with cumulativity would be able to handle = what is said in the above injectives paper. > > When I say "would be able to handle" I don't mean just "accepting the con= structions", but also present them to the (mathematical) user in such a way= that is both understandable and usable as a blackbox (by quoting published= resuls). > > Martin > > -- > 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.