From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a2e:9d83:: with SMTP id c3mr7652925ljj.90.1589124198007; Sun, 10 May 2020 08:23:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:9397:: with SMTP id g23ls1805232ljh.7.gmail; Sun, 10 May 2020 08:23:16 -0700 (PDT) X-Received: by 2002:a2e:a549:: with SMTP id e9mr7655459ljn.283.1589124195980; Sun, 10 May 2020 08:23:15 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589124195; cv=none; d=google.com; s=arc-20160816; b=BKZ7NbCyiFKT2a0K61atuWzRnzUym355CItBX1RtWV+Y59jZpm5dxHhyn+v7vIwZSq ycbod/NIGiG1q9fFBBxCVwmjH2L/zyOG1USerfBdDRr8ThRlqQ68aLnd1Epihg8o1gco Fk6FbM0VGqP7T9moNYVN+yOCp0KQcaaEUMingpcy/PC2GgxVV8MIUzXQtQ2VIt9psW2S d/S/9caetbYxcjfzEWr915yr+8GiiYIcuCJOVUcsArjxt0nSRl+ofJNu6XrepFZHQo6d iT+oLlXKdo2vGtJfVa0BR4enrnaTcuEM8W00vb636bZFVKsn10bqCe5z5Jr8H8PAOY26 c6qQ== 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=SxHWgBFiKn+UGwWWFFVNmtkrSjjvPgocTS9Gvukculo=; b=RR0wRjwqli01hHQooq3CDO4UKQ9tPCp4j0Sw/sJB57wSwr5iPGoViCsz2JnQMIzQRt 1prhP+3CADQ6akeHvvwcusiD7+VkQ+xqM0dt3l3OslD8L+lohIAeYO3uFFcwREUUxpl2 EiFOcH4nCAPE6IY7pFtV9Y5erSRdRz3XYkAlcOjV2HLCieO2335Hod07he7XOA+tTvz4 uY4cZmcKE/pOH6I/tJ2wJPosYNpatIGJ5DsXPQOJEqj4CwdsfbmV6d9pkXNUBFQ03Sww v/0A0ni9mUz1F8T/9yk+s3B9aOiK3nhgKwD9CF0GIEmJNjHNo2TxjblOYpAMDF853uez 7C6g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=KPxLr2Qj; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::32e 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-wm1-x32e.google.com (mail-wm1-x32e.google.com. [2a00:1450:4864:20::32e]) by gmr-mx.google.com with ESMTPS id v19si64708lfe.3.2020.05.10.08.23.15 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 08:23:15 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::32e as permitted sender) client-ip=2a00:1450:4864:20::32e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=KPxLr2Qj; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::32e as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wm1-x32e.google.com with SMTP id g12so16044908wmh.3 for ; Sun, 10 May 2020 08:23:15 -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=SxHWgBFiKn+UGwWWFFVNmtkrSjjvPgocTS9Gvukculo=; b=KPxLr2QjtkgC8UosyTzbtZ4eJ2UngJJyLcb9NpiEiga1bBQLjvd6F9yoWfRDVPNzFt uLzaMNLbag07GlVsEqVTFIoX9GiJmXa0bj5IzpXasUwWvZpfDMzjF2eWy/S4vwpSWqup JJ8dIo0hTqDwuzbb8ndC85qx+k0jjGsZW+Rw+z82fEt/g0JDFI3Lb143KYUnIyWAiP4/ E9RgpuOFp34VaC2wwyOBURE5A3Ee8JSs7vKVdf9Lnzrxo/dYH+ZBDabPjbze32FCOmn2 jvpVCIfEuV7suZCVSqEv/PgvR1gi3P8HvsKVCnPIBqw2oF6E9hhgY3LMUE7Io14Bc8oE db6w== X-Gm-Message-State: AGi0PuaEms+V5V/7AvJ4NQp00XH+S5GbPGN7hSlBTPfeV9zN3yTFYCdc 8hf2hslrzEsz69YtnJcfjKlxtUMUD5MMSg== X-Received: by 2002:a1c:9c0a:: with SMTP id f10mr26615160wme.139.1589124194883; Sun, 10 May 2020 08:23:14 -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 g10sm12657752wrx.4.2020.05.10.08.23.13 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 08:23:14 -0700 (PDT) Subject: Re: [HoTT] Identity versus equality To: Michael Shulman Cc: Thorsten Altenkirch , Jon Sterling , 'Martin Escardo' via Homotopy Type Theory References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <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> <3ec2f134-cbd4-7bfd-0a69-efb734a4a231@gmail.com> From: Nicolai Kraus Message-ID: <9526fc07-cf21-03e8-1c68-acccc2941117@gmail.com> Date: Sun, 10 May 2020 16:23:13 +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 Yes, I think that is one main motivation for this axiom (that you've suggested in this form :-) and I also believe that it was Vladimir's main motivation for his axiom "exo-Nat is fibrant". I think the two axioms really serve the same purpose, but the "cofibrant" version is much more harmless. On 10/05/2020 16:16, Michael Shulman wrote: > I forget -- does "exo-Nat is cofibrant" imply that exo-limits of > towers of fibrations are fibrant? That's another useful axiom that > holds in models and might make it easier to construct coinductive > types with judgmental computation rules. > > On Sun, May 10, 2020 at 7:52 AM Nicolai Kraus wrote: >> I would guess that "exo-Nat is cofibrant" justifies the coinductive type in question, but not its judgmental computation rules. And the judgmental computation rules are probably the very reason why one would want this coinductive type. But this is just a guess. >> -- Nicolai >> >> On Sun, May 10, 2020 at 3:35 PM Michael Shulman wrote: >>> Many or all coinductive types can be constructed, at least up to >>> equivalence, using Pi-types and (some kind of) Nat. Is there any >>> chance that "exo-Nat is cofibrant" could be used to justify the >>> existence/fibrancy of the coinductive types you want? >>> >>> On Sun, May 10, 2020 at 7:20 AM Nicolai Kraus wrote: >>>> 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 >> -- >> 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 HomotopyT...@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBr0Zh-uLfEZCXUapK5KHFDxkzxyvLW22zyjmrB8KmWtYQ%40mail.gmail.com.