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,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wr1-x438.google.com (mail-wr1-x438.google.com [IPv6:2a00:1450:4864:20::438]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0ffe72f0 for ; Tue, 7 May 2019 12:42:06 +0000 (UTC) Received: by mail-wr1-x438.google.com with SMTP id n6sf13163675wre.18 for ; Tue, 07 May 2019 05:42:06 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1557232925; cv=pass; d=google.com; s=arc-20160816; b=JQTp27cB6u9Crjuc0KDWqnuVGo97jfF1RAj76E8caJLFdfHZKWrtCMIQoODV5DFpab Oq4qS2BLYtqZOSoJztl24UYebZ2quREPFs/yH/B4enoP20yqxu+oGg4eFsT61g9IRHdo yI33k0dxwZOPpBWMFrt7uH/LCoF4mwpFB/6ZdrQxeoGobEIuc2iD4h7olqJO9I6NakAo EKgMYaPKZzIdL1X6brcnCQi0UXKExNvZbsqkznJLzaj40Zlm1m+0RGder8q7nukjZX4w GXMtJfJcmyj61OYq0Gevx49pYOcwkLH+LZj2CZjJpLmGU5+sQm+ig21vykBrjq6LIk0N pNtw== 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:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject:sender :dkim-signature; bh=UDSNg7Ml4r/HFBsEem7ECWaah0YogrOUVrcXREkXgIs=; b=dBfYG8GY6qlnOahs5gYcKpyfjlJStZVzWgCKk66FSKC6MKvPLIFTdlGkFOXfNVaheE CHpCyAI0jHZ34uMHDkd+2l78lufIEl8ihiQzzp6byMh0lcIAGL2YOAhYj100Ki98y0wy R63sy1eeHcwQvx90IgOvNEs6TOhggwvql7PXcY4GaMQQS7lwy4MRDYJZS+O3Ka2rKuQF JlPSxg8IMhJgcOrU9JC0dPBR/tyq5ykTvEmPd4/kQUbIRH5+unAoQ4poPV0SOM8rM+Cn aM/4FZ64mFoRc5g27p79ZgFkon6JC7PtEUGiHxsg8NTSFRX4MbdiVVJZxqPKp8uyGQoV qkXg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se 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-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=UDSNg7Ml4r/HFBsEem7ECWaah0YogrOUVrcXREkXgIs=; b=btWqQ5uZz3HqR+ayvskcc/0AXHmbno98hxBY5UbnzFNTu1orXDNOeInMSMmStIraN8 gyFhsaFfIB8+cUH/PrKB6f/saIK8+JF70VZ9Xx2eMupnBm9Lnay2GyE/Bu8FC4HR7G83 hSUPTrufySl6P2Ii9Rx7Mf5SZhWQPJZlf6+7Vvv2RSwigStomhzQRlD/ejp1GURWfhaW 3+dXDsGjj9S4fajr45LVnR0LsoRxufp8Z0QaM7zPJRc0pQpXVi4qHQZUZ2IAPH1BuV0i 9bZ1Fyykg2X534GHE41sZbHFMykOUeWoRi5gwITDA/HihQq05qpULKY9hvUxv3gJ2wmI ITew== 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-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=UDSNg7Ml4r/HFBsEem7ECWaah0YogrOUVrcXREkXgIs=; b=DBbEDFjFHY53LrDFWMFeNAr2TC2Nd7zuFqmFnZS8rjas6pwaNXwxks3ZxY8o0fNvbd yllkzlRXOiLIcZqgGBKuL5Ok+Pd5iCYTj8EmWoBi9BlKD7SS0pGjop9w1mqiGYs0+RE5 ydfM6zEsAeBbslkNJahZgIdRmE8btFE0dmMjuq2Wy4FQ62w2kj4hzck1SieNMqgxr4NK kVXllVFEAHueb2DaaJub09oAHEPaOqLwh0Gtny+psyIPSH5m5WFmeW7bDZHHQWFh7qdx oq+mKcLHsmWc89pEuS6NBE6ZCXuhfO9EikXfD2JOjnPJziS55IIxOJfOycT+D9YnpAnn hpVA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXze+AuUXky1NXx2kP3of2TCS/8Pb0fWfYwPGUiPuIDoLa/xgIh 03kA95Al1If1WJPAjjlrm4o= X-Google-Smtp-Source: APXvYqxXi1lVc++6VOvCIvLfMWL12AFvlCO85rf0F6fj5LlLkJpAH22VgbC4da8oewEfuJEITzOTjg== X-Received: by 2002:a5d:4d46:: with SMTP id a6mr3607822wru.142.1557232925229; Tue, 07 May 2019 05:42:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:b406:: with SMTP id d6ls4834199wmf.2.canary-gmail; Tue, 07 May 2019 05:42:04 -0700 (PDT) X-Received: by 2002:a1c:cc10:: with SMTP id h16mr21596762wmb.39.1557232924639; Tue, 07 May 2019 05:42:04 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1557232924; cv=none; d=google.com; s=arc-20160816; b=pTY+J0WhikDj1Mp+r8kQhpQguJwwqnmH9Kz6dISDMmhLe/SpaGdN+1ZGycNpLG92BL 6Gz5vSp06zBbZl5qpdPhe0dPn83zhB9PfQICUVKQy7G1WPL+Mv2TEXiBwaCXXyXmibMW ic1aWx2nDT2DJS41mUNg9pBmmuIq0BjYggme3hYjmjB7hDvg7iysBT6AZYDKM93tVSdr RJN/dcOgG7kbhFj6xyrfBaabGR9ZZHWVplqBbwijaMD+zZIq3D8WuC3HdhTprFtwDyIO zHrsg2NQgzGx7ROeuUTjWg/8QNK3hPieasqmegYAxWS0fwEkU9HpYBvIfpQEU7xXG6Z1 sz5w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject; bh=VcDrYmyDCrIMujLzmAZ0cc0FGbKqTTjDOY3kFstzVOQ=; b=XJ5wXM8gHgQy3hD8tNk0F71ehLHwkud8RucfelIch75AvoQq9IAg/+Uq/maXyhhNzp ltvfZTKpsmZLnRFb8I6wfl0yk2c4JQ/3ptgKm7IQaX4FCSndWioO4FT0Hww/sYKMiPtF m3HheU1IrmpB9VAj0vXAqghGLL0NyySe2MnaDRu2YAyz/lqqS1VIODj/bGsjOsRpnHNe T4n17DLvJ0L1Pn7O7Pd2nM2E3yrxNhAYBgIcRxOA1RbPQKKJKe14w4UvFSYcRJH9+Nr0 3KpzmsK+TDiLP4agWtlwJohcgOSfIv33wCpd7JiMbG45va9sYUjHqTWJ97wNkRwyUZoj OEkA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se Received: from stark.ita.chalmers.se (stark.ita.chalmers.se. [129.16.226.131]) by gmr-mx.google.com with ESMTPS id j13si35502wme.1.2019.05.07.05.42.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Tue, 07 May 2019 05:42:04 -0700 (PDT) Received-SPF: pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) client-ip=129.16.226.131; Received: from [129.16.22.134] (129.16.10.245) by stark.ita.chalmers.se (129.16.226.131) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.1713.5; Tue, 7 May 2019 14:42:03 +0200 Subject: Re: [HoTT] Injective types To: Homotopy Type Theory References: <9a1466e5-1c06-4ae2-abc5-d3fbfec5c851@googlegroups.com> <7104f60a-7dba-4574-8629-860c0bc31967@googlegroups.com> <2b380e43-8623-4900-b529-1e267155562f@googlegroups.com> From: Nils Anders Danielsson Message-ID: <5fa99a80-56ed-abc5-d64f-876c192bca6a@cse.gu.se> Date: Tue, 7 May 2019 14:42:03 +0200 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:60.0) Gecko/20100101 Thunderbird/60.6.1 MIME-Version: 1.0 In-Reply-To: <2b380e43-8623-4900-b529-1e267155562f@googlegroups.com> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US X-Originating-IP: [129.16.10.245] X-ClientProxiedBy: tyrell.ita.chalmers.se (129.16.226.132) To stark.ita.chalmers.se (129.16.226.131) X-Original-Sender: nad@cse.gu.se X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se 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: , On 02/05/2019 22.46, escardo.martin@gmail.com wrote: > I can confirm from a 26k line Agda development (with comments and > repeated blank lines removed 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 assumes 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 are *extremely > rare* in practice. I once wrote some code where I made use of univalence at three different levels. Does anyone know if one can prove that univalence at one level implies univalence at lower levels, without making use of cumulativity? -- /NAD -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/5fa99a80-56ed-abc5-d64f-876c192bca6a%40cse.gu.se. For more options, visit https://groups.google.com/d/optout.