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-x239.google.com (mail-oi1-x239.google.com [IPv6:2607:f8b0:4864:20::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3b19b9f0 for ; Tue, 30 Apr 2019 23:05:56 +0000 (UTC) Received: by mail-oi1-x239.google.com with SMTP id w16sf6285282oic.10 for ; Tue, 30 Apr 2019 16:05:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=KHEeNFDW4yl+eZPN9BvFol5Ko8Y0Lg3/sLkYqnAi8+k=; b=k8mGSMWtlKhqmvAyvRbcoQAZ1B74GItEnHsGYl+1bU4eP/AcWXJhFQ/nVo3uZEQunb Zzc+rjsV4JkBYDWLpkpmKz32FBB+U89Ey2x4XuGUrvN1X1c0Yt9AQect2fspKGpyn+Iq CdzTaB3tEr91n0e1sw/U2cQG4CVd5wB6iCCkdzlHtTyBRUJXJqAcYaGzj9X0MSqnLDj1 q3iJ/V7Z0iklZbujg3XueQngnrSgrnkhWRop01mXwYvMdVju8MpSqs8r2PNDcXtlP9Au lX5AzU76CUKOTUMmo3M9bOz8bDHHFEuX+h4DpeTWjKx90mzsmbrvtB+ifJ8RTuvYR/IL gy+g== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=KHEeNFDW4yl+eZPN9BvFol5Ko8Y0Lg3/sLkYqnAi8+k=; b=N6nyZapCD8N8aLNzSdToJ6shQ5uT2d9diDi2IcwWTl+n8YdOvbi2mkQKxKUbFuub5R zz2uVOAAWrO6pnAhK5GjA2sjPee1ZtqwgoHnsqaQmbTchHAHLjnPhROyBJapS4JhMHwG oF1JcBoECA7hAKkegYEBaNCZGgbSH1d8yj9v3gyQepudswuIBzGSnNPpO2GA5QWD6Pgp EDsn6yWPnxEAOxdC4OJ5dn8Hehzj6/r1VOtRk29hGN74Zve5WwJFzgpsmCekDD0qmRXk SbMlkltRP10WlQ0Rm889CS6zEQUo0Oiou5tohNScv1DuRjKY6WHexnQRL82PapXv2MCb mQgQ== 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: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=KHEeNFDW4yl+eZPN9BvFol5Ko8Y0Lg3/sLkYqnAi8+k=; b=lf59mw9npLv+d71LmJ8ddX/Xac6ro7WknshnZ/f4TRWw5q7rrdzejHD3zON4A7eEiO rfHAQ0DHif0HPhPPu8mWGMtBbHfed/cwobwyRIJyztu3ODmL9Z+4oXbE8z8Joql2F1D3 fYs9bxl6glBCI6QN9K3Ula8jgXXApAOHgBzObVg5+pDcC8qzAZdkqlQ6eijsiC04SxrE 6YwEdJvWiuXfl7jPZyyE3hPkpbu/Fkil+kinziLwoCEOzup5jpw4NQ7/SPNt4XSwUFog uWRT4F1wFLmMJAHGLjrxSN06hRh2jbdGTbsrk356bLKFbMbhKKDjI8bPGtwtpJea6Gc+ Bwyg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWoIBkdmci4+5hPme2SCyPJlbP5qn+1kuxvuXAKq65u7UpfY9BA OU5ovMUcKo9LVYa44dLe7k4= X-Google-Smtp-Source: APXvYqwxtFfJhqJt13pJpKXk9aAuMD898MsGnE4VBJiy4dNluvVT2Wr7KkwKE4bqRbFuZ/wOp/Cv9Q== X-Received: by 2002:a9d:70c1:: with SMTP id w1mr1571265otj.312.1556665554210; Tue, 30 Apr 2019 16:05:54 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:39c3:: with SMTP id g186ls502629oia.15.gmail; Tue, 30 Apr 2019 16:05:53 -0700 (PDT) X-Received: by 2002:aca:3746:: with SMTP id e67mr4649691oia.37.1556665553075; Tue, 30 Apr 2019 16:05:53 -0700 (PDT) Date: Tue, 30 Apr 2019 16:05:52 -0700 (PDT) From: escardo.martin@gmail.com To: Homotopy Type Theory Message-Id: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com> Subject: [HoTT] Injective types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1863_1368607080.1556665552245" 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_1863_1368607080.1556665552245 Content-Type: multipart/alternative; boundary="----=_Part_1864_1674196049.1556665552245" ------=_Part_1864_1674196049.1556665552245 Content-Type: text/plain; charset="UTF-8" I would like to advertise this paper, which investigates injective types and algebraically injective types, and their relationship (https://arxiv.org/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 there is only one universe (this is called typical ambiguity). Based on the experience 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 am 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 constructions", 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. ------=_Part_1864_1674196049.1556665552245 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I would like to advertise this paper, which investigates i= njective types and algebraically injective types, and their relationship (h= ttps://arxiv.org/abs/1903.01211).

In this paper, it is i= mportant to take universe levels seriously (for the reasons explained there= ). In the HoTT book, and in Coq, the universes are taken to be cumulative o= n the nose, and we pretend, notationally, that there is only one universe (= this is called typical ambiguity). Based on the experience 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 am not sure how typical a= mbiguity with cumulativity would be able to handle what is said in the abov= e injectives paper.

When I say "would be able= to handle" I don't mean just "accepting the constructions&qu= ot;, 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 &= 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_1864_1674196049.1556665552245-- ------=_Part_1863_1368607080.1556665552245--