From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a5d:61c3:: with SMTP id q3mr11980780wrv.405.1589120437483; Sun, 10 May 2020 07:20:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:4103:: with SMTP id l3ls5447553wrp.7.gmail; Sun, 10 May 2020 07:20:36 -0700 (PDT) X-Received: by 2002:a05:6000:110b:: with SMTP id z11mr10723551wrw.16.1589120436112; Sun, 10 May 2020 07:20:36 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589120436; cv=none; d=google.com; s=arc-20160816; b=qGwLvjFnDVhn9SUbWMBt7KO0KirquAzxbtbGFcE2nwQnPbftPtz7ibODqqk+EvvWbi HBfipIWhgvydT4D7GvICnC5fGwPblcS6nDa4I75+cQP1sKPgLmaAh+ku/k91R4iZ3L65 3dwICS6zq34ejjiADlDfuvhXwATyUt22m20Nl59OQ89IPX/v/ebJ8JYyhu/vfMzXStSV 3Hqq6yV740I2f26fJ49etsIwR/FrDRY0A+pzgsbZOQQfd7DGE+UXkMAHGcmszu9+mhmO 5jpPLRo6EMbRYUeiIk6XeP0+Z88yFQ46449wVJJcz1RB4tHK+38OUhzieX904oCU7g5Y Tjfw== 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:cc:to:subject :dkim-signature; bh=fdQTGsfED5gHvVtw53o5kiAmRdnUw3D4E5PYRxJ8DAE=; b=jAOpdD3Siojr2hb8WkgJz/Prmf6PYOtvvRtrExSP1DAgtolSG6zI4jbg9dwwYEfQbI JrQqqa4al83q3KlhOc7P4e1NER3ENFJy84Yi6wQHl0jP99Cce6B6Ck0tTVa9vIF7ZXpc zHEWw8DWzpKYRA5wo/CJp0h8/xJ9zwBBVPqlUhdV/F9BQjUDoU9jTDbsEmuDoVP0BZbr b9hDnOswXh/mqevL4iw6E8GAhdrAdekpbGlbjasJCr/954YDXHsPrk0ZS7KyEepdRfmW 25lKWcNlomVLF8t96YzzgK/Cwaw5DYoYfvZGCEbbYkfB7qp9BxZmGNRaYXY0JFkIuUV9 BnVQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=DJS6J3rC; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::434 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wr1-x434.google.com (mail-wr1-x434.google.com. [2a00:1450:4864:20::434]) by gmr-mx.google.com with ESMTPS id o19si136409wmh.2.2020.05.10.07.20.36 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 07:20:36 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::434 as permitted sender) client-ip=2a00:1450:4864:20::434; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=DJS6J3rC; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::434 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wr1-x434.google.com with SMTP id j5so7584912wrq.2 for ; Sun, 10 May 2020 07:20:36 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-transfer-encoding:content-language; bh=fdQTGsfED5gHvVtw53o5kiAmRdnUw3D4E5PYRxJ8DAE=; b=DJS6J3rCfTI+tK2J3kmxhzuUXtpr0J5YWL2qGEYCjVTDZNx/r0ZKmUWkdhVIfm3Nns y7pNklbrkwrQMpK4hU5Su7r4pKC1W25KagHIZxNav4tb7pMc3dkNIKqFW3pJs0dDT9MF CK4/yuCFGDTYMdQ12qgoadjx9WcgE7s4DVnns+aThn+joGS/+aLv1XNkd2gaKDpDvm6S SgEn0GCNgvcKBJy7iiqiYsxWgunb6F62EFIMhLswmGO/Hnzwa8f7z7Pq4FmOyLZccCVq uhJuLvgOfqFG246nlhV7d6Nw6RwGZkdXpY27MAQKuvr0dNRlOYIu7gI1BujwVVEh34if /k2g== X-Gm-Message-State: AGi0PuY82tCbaFC48xeDq+DTskKWA+REPlFvpcaJm7GUJa+U2KHYZHHR AHmFE64JwX9pDgD5Dx0Db7WyFAFdeLTJ4Q== X-Received: by 2002:a5d:684f:: with SMTP id o15mr13204712wrw.89.1589120435472; Sun, 10 May 2020 07:20:35 -0700 (PDT) Return-Path: Received: from [192.168.1.67] (37.67.90.146.dyn.plus.net. [146.90.67.37]) by smtp.gmail.com with ESMTPSA id v8sm13190214wrs.45.2020.05.10.07.20.34 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 07:20:34 -0700 (PDT) Subject: Re: [HoTT] Identity versus equality To: Michael Shulman , Thorsten Altenkirch Cc: Jon Sterling , 'Martin Escardo' via Homotopy Type Theory References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> <154D1B4B-6881-4269-8BA1-1CE8EBB0BE0D@nottingham.ac.uk> From: Nicolai Kraus Message-ID: <3ec2f134-cbd4-7bfd-0a69-efb734a4a231@gmail.com> Date: Sun, 10 May 2020 15:20:33 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.7.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Content-Language: en-US On 10/05/2020 15:01, Michael Shulman wrote: > On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch > wrote: >> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type > We can certainly *talk* about simplicial types in 2LTT as exofunctors > from the exocategory Delta to the exocategory Type. I assume the > point you're making is that we don't have a (fibrant) *type of* > simplicial types, whereas we do have a fibrant type of semisimplicial > types (under appropriate axioms)? Judging from the rest of his message, I believe that Thorsten was talking about the direct replacement construction in Christian's and my abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant", this gives us a fibrant type that one could call "simplicial types" (and Thorsten does). But of course it's an encoding. If we decide to use such encodings, I fear we may lose the main advantage that the "axiomatic" representations in HoTT have, namely avoiding encodings. (I mean the "main advantage" of HoTT compared to traditional approaches, e.g. taking bisimplicial sets.) >> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist. > Personally, I think the best axiom to use here is that exo-Nat is > *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy. We > don't know how to model "exo-Nat is fibrant" in all higher toposes, > but it's easy to interpret "exo-Nat is cofibrant" in such models, > since Pi-types with domain exo-Nat are just externally-infinite > products. I completely agree with your preference for this axiom :-) But Thorsten does has a point if we consider the "engineering level" that was discussed earlier in this thread. Allowing coinductive types with exo-Nat as an index makes it possible to use your paper (Higher Stucture Identity Principle, arXiv:2004.06572) and get a construction of semi-simplicial types which is more convenient to use in a proof assistant. -- Nicolai