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_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wm1-x340.google.com (mail-wm1-x340.google.com [IPv6:2a00:1450:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e8d2dc27 for ; Tue, 7 May 2019 13:51:48 +0000 (UTC) Received: by mail-wm1-x340.google.com with SMTP id y189sf10739285wmd.4 for ; Tue, 07 May 2019 06:51:48 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1557237107; cv=pass; d=google.com; s=arc-20160816; b=iiFxzuEPRc3FHCVkrnhbkIYzjzr98y5jXSit4KQ2mKAlfHMYvQ1/AcKn9e/ljxxl6O h6b/1iKggTTJ3qosVQ67vU+aBKalAsjmSL0Y6LPtQuHiZT3s0bt4wD452IEsZvUVzJuQ baWGkixfwwxm0sUgZqpN17JfFivaSpA2s7+ytwUJAzqEL+ViLdcnB4o+kX52A2R6/QDt xntUJpeKNTxnx62vY6W/Zif7y/33fTWVlISXi6R3oA9sG6CEahW/+bRcrVj83JVRy9s+ RKP1zIS7kRW1LL1OAN5yPInwduycem/qeZb6sMBACJrIwmnQEBifuacLdumL7xEmnhQt 6jsw== 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:dkim-signature; bh=N40pWdJaqGwUaBNWBCFOXHpAFld0DXmqcUlCTNhs+l0=; b=laiC7gepBFwoPNIYwPtk4BV/fEVmlqPAmxWyRFNiC2/sGQ+0IW686WbqLFdeAvAMsc /B8talV/CUBrGPkXYCRkg1eBaWA0K/RZ/YILOtwrN5drHLwxsKBxOijpLubMz0JM+orx jB6YJQ7klXvhsp0O/lpi/7wWh6+hdwtGHsSj2QasbtOrHGMGgbMPySylY3fIg1YRtZdt H2I5yzioO9q3u6tnNUzMOwMOonXHcOS/tp4WCF8VZeqMs7oFQafX8gDQ6ZrrxBtofnkK MmC2/grksEpp7KTcyTgme86jamiCnqMru3VXzkU8oujLwaq/H6I/w+HMAbtRGg2lEixK fXYg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=guLOYmBa; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::331 as permitted sender) smtp.mailfrom=andreasnuyts@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=N40pWdJaqGwUaBNWBCFOXHpAFld0DXmqcUlCTNhs+l0=; b=p7KPaJQHkK6tmwIklRisLZfCzKQddPa63lvgnGU+Bdm9Ok+9JL7f8ArATHLATjHHFj DvlED+4j34wqaggDU7iIj3XXi8joVFZCo8ymGUS2njWlgKy5p5sJmfUMrUx+r3JujPDY FDv9F2WfpwzPyYOE+vg9OsZkA17ovZq2hSyYObSkm0y/++wr9vcjso1enBhWIrRjKZHY MIpRWaJ0n7TeOXE/rkzAyUaDq6LkDSAm5ztaRlrka8hje/EPvxzieGFZg5dqi4MJwUim JSVxv4d3vyKM7F7ZADmckPVSirrHReDvl8ooG9ORFNC/Gifx3WXMKlLMEbrqmdKVIVVv 8vmg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=N40pWdJaqGwUaBNWBCFOXHpAFld0DXmqcUlCTNhs+l0=; b=DF6gDfoZbiff5X7T1p/zmih2djRJhkO5knFnjp5NnPkom4INpOOvkY9FNmD+gis3ne RyKchmlHA0djhgbyNAaq2BEV/LumSIV9UQgy7qIYDy/9yxWZNO+D4QYn6qCGmWcs6oSM TeomyNerSK7KHEO6VtWPiNdVk09cd1hWZ1wIftfY/6ShltxeTub0X+3PAIbiXl4eRf51 IZ2+RthEouWe6mu6U54Qpym9bZsP0F21vqI1CFlEzlF9YPqHRxWlxG0pI7K7j/8GZtL0 5Or3vIhRXX6jtLcyawXngAOHs2f0hYu87s7WWpcWhSSY51EJ2lbcKbD3iAZ6XiVV2kk+ YaBA== 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=N40pWdJaqGwUaBNWBCFOXHpAFld0DXmqcUlCTNhs+l0=; b=RhNPKnnwO2J0EbM+qNb9EXX3vt1i6xTBF2b7pDJSUhjW3YDi3/eSHqWWbTrw++lbkX H4b0E97I6XKLIQZjuAXGTsjB8QRlQ1hTG6KaMn2PmYtF4Uhzbg+TdXQjjvQaApOTB7Ya /hHACyE9kwAsO1iDE3QaeyYQgEkXYBd58zwlOruJm95aACrdFoPhm7641Dq4Q73Kehlh xgqlgYUr9IlPDzuqYHA4YTB5M2MzdcgVkl4x4ceh/19MtMF7/4ruOOqwse/z9PpgR1Zz QoFwVJs7djtkO/wK228TMEk9yUDeh5KPcziSOWTfWJfqmorbFHmYKz/seQQr92t5T0EA xvCQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVUBMLmsXVv/OWQGMGo1FyN/uaGWdKy86J+J41Gqhv2BPv28a18 aWrVjyzjFHYIKpWGGOy3pUg= X-Google-Smtp-Source: APXvYqwV38T47zVgJCNGTEISWl8kRCKY2JSZ/IfCkLJnPhwxRYcbAmBEsc65kBtNFGtbw1VqaJDCSA== X-Received: by 2002:a1c:9eca:: with SMTP id h193mr3004595wme.78.1557237107677; Tue, 07 May 2019 06:51:47 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:2318:: with SMTP id 24ls3091724wmo.1.canary-gmail; Tue, 07 May 2019 06:51:47 -0700 (PDT) X-Received: by 2002:a7b:ca42:: with SMTP id m2mr21175812wml.35.1557237107186; Tue, 07 May 2019 06:51:47 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1557237107; cv=none; d=google.com; s=arc-20160816; b=R0KPda8SmDuvPtJ8D6tFW++BQwUv5pcusVgUNwB1ujYFbvIDT5D/LLjJBEGs5U9U/R /hgz21dkXeRQKv+by6LWlu73PZeuJUjQFb4sZ9Y2DG1Ku+9jH1XY9i1u/L7Rp00P3xIZ pJa49q36W1IBtGJDNtmQ0iJtdiaWrTKt2+RCbDdYOCV4HSRjuyiKnWMw0bPlbBnBa9IM Vu4NND8bLiYTNFg/GkrudySIzmP9cvuKfAlveh2ELEKq+QKNzRx2RMPQcT9GN2gx/4zL fsveYzKuIzju8WdvpyYjAo7s9lvdUjCOSBmmnGnkVsyLs+gyPeF3wGQlUnOoeSLET83D fmJg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :dkim-signature; bh=yP8ntpHvgEE7r0rCf2GTOg4pNn36xNiC+ctJn6jbz8U=; b=PstnfDMJcsek8aTv6q5WWyo4k69H8/ZvxLGpQGSej19dtB644+Bl0W8fObfsE7tN30 HDU/KChnJGMQ9I2I74Bzi/E7tuU9v09CBL/vrOnbzHW76PwoB4f4D0IgONRej2RE3ajY ORH9wDnYZYNReNSPFvh3B43lZSaQA/J4hqVCgkhuzzV5phtIglYKwPlz3j/YtJOO4ubL guXIR2XSyOB+XeAL/AQ8iHVLiun3VVr28fRszkiobrp9V9LYPDiD8FCR80kcOgNXRbtj a/l6krtcKtyPcWtwUx+77nAZZ0ZEi+8kLBpAzkyOuvW9ji5C4Ca9SeHPJWzMJA99P1gm G6Yg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=guLOYmBa; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::331 as permitted sender) smtp.mailfrom=andreasnuyts@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x331.google.com (mail-wm1-x331.google.com. [2a00:1450:4864:20::331]) by gmr-mx.google.com with ESMTPS id v1si564414wrw.5.2019.05.07.06.51.47 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 07 May 2019 06:51:47 -0700 (PDT) Received-SPF: pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::331 as permitted sender) client-ip=2a00:1450:4864:20::331; Received: by mail-wm1-x331.google.com with SMTP id o189so9644428wmb.1 for ; Tue, 07 May 2019 06:51:47 -0700 (PDT) X-Received: by 2002:a05:600c:24d0:: with SMTP id 16mr9249289wmu.21.1557237106694; Tue, 07 May 2019 06:51:46 -0700 (PDT) Received: from ?IPv6:2a02:2c40:500:a006:f995:653c:977d:cc1? ([2a02:2c40:500:a006:f995:653c:977d:cc1]) by smtp.googlemail.com with ESMTPSA id r2sm31904045wrr.65.2019.05.07.06.51.44 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 07 May 2019 06:51:45 -0700 (PDT) Subject: Re: [HoTT] Injective types To: Nils Anders Danielsson , 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> <5fa99a80-56ed-abc5-d64f-876c192bca6a@cse.gu.se> From: Andreas Nuyts Message-ID: <49d95599-153c-d641-4ae9-a3f7c02b1cc3@gmail.com> Date: Tue, 7 May 2019 15:51:44 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1 MIME-Version: 1.0 In-Reply-To: <5fa99a80-56ed-abc5-d64f-876c192bca6a@cse.gu.se> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US X-Original-Sender: andreasnuyts@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=guLOYmBa; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::331 as permitted sender) smtp.mailfrom=andreasnuyts@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , Even with cumulativity, that sounds suspicious, because cumulativity of U in a bigger universe V does not obviously give you a map (A B : U) -> Id V A B -> Id U A B. The J-rule does not allow you to build this map. On 7/05/19 14:42, Nils Anders Danielsson wrote: > 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? > -- 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/49d95599-153c-d641-4ae9-a3f7c02b1cc3%40gmail.com. For more options, visit https://groups.google.com/d/optout.