From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:c194:: with SMTP id d20mr11520787pld.256.1589127206705; Sun, 10 May 2020 09:13:26 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:d049:: with SMTP id s9ls2876504pgi.5.gmail; Sun, 10 May 2020 09:13:25 -0700 (PDT) X-Received: by 2002:a65:6641:: with SMTP id z1mr6588944pgv.113.1589127205220; Sun, 10 May 2020 09:13:25 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589127205; cv=none; d=google.com; s=arc-20160816; b=JIzREzCeD1JK14WnqNi+cRG99G0dpu+sENYVoDJWhcuL9oQ9FKxwsLm0Vihi2jbl6O NjGaf3opImyXG3zBR5P1Yy4w3nVA+Cwe9Tb8s64Pk69ueUm963MHCyVbLb7nbNHCmws6 DQhYtlaWY0kOYOBCcuo1geFj5/kLadByjUwfFZ1jbWOk7FIr9TSoVvdTrK9P65cVtWpc YbadnLxavwAu1fDfR3YBQz5yb8vhNajgZgTkF/PKUNhJsZo8uXQBpKEl6WrbKj6wH1AZ ZweVKNvVlNX9OgjP5+8xFMLmhsWLYSTx5mTH/t8Hh7rAKnejOMkPpgxMrK1rHZycBv1c Lkpw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=34cpnH14UjLkrnJezFw44CcnmdDqF7ZtIK2/v0kpWbY=; b=an4tQsARf2FMxnNgOmIS3+gbveaidvw+IFY4lQWYxyZjGEXhYmIqddM0xdOth/zdc/ HELhG3sS7HVk+ZrRpvgChLU1Fy8fVDX1Jven6j7d1Evzq1HlcZVlCEObvxdjxcGQQxN8 Jwg9FhCKdpxPOnJxef1Ls7zAccNLtdSqIc6IB4T/5kg2WO/tjSSt+a0dORGEuLUpSZUI 2a4pCtOLNbh1Dud732RXxSjylh/kIhl8HaXxLb7KmaDpduUFC83pcbTZUXqskqUQncou kqEfsWyfE3Kr+JcfrFlBAzjrqDkF/ZD4O1645K7UASNu4FWXt7ubj57mwvERtfCvBAqi 8JXA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=RL1IpDvZ; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::c2c 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-oo1-xc2c.google.com (mail-oo1-xc2c.google.com. [2607:f8b0:4864:20::c2c]) by gmr-mx.google.com with ESMTPS id ft5si554908pjb.3.2020.05.10.09.13.25 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 09:13:25 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::c2c as permitted sender) client-ip=2607:f8b0:4864:20::c2c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=RL1IpDvZ; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::c2c as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-oo1-xc2c.google.com with SMTP id b17so1434081ooa.0 for ; Sun, 10 May 2020 09:13:25 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=34cpnH14UjLkrnJezFw44CcnmdDqF7ZtIK2/v0kpWbY=; b=RL1IpDvZf5srWmiggAiP6Jb1V2JfrrRkYufyiOEzmKiPVM8TOg+FJXnuVP7Hr3MRE4 d3VFjdpb50zqx+evJ6i4kJEpfsc8Jm4UG74VvGOS8HUKSeDc9xb7cz/DaEWyZKVjXMW/ X9CqD217lShm5q7MKom+QTWnmzNVda7FllQ1irBbxmlYlf1V0xuuisAq5RaxvsdNMtLJ CoEw1u6+Z+JKFL/bzsCkLsb5lXHg7wljWYVYL2Cf6ex5ZrrCDTOtKIBoRF+sWNAutOHe uD7UUk4AFCWvrSG4+8pGXNwapgGdg5c7ZPZeLIvD4cLObt8tsQB6v5v/3CAsSZgxizFO /lLg== X-Gm-Message-State: AGi0PuZFXGQOXLs32FJ9OMLvG8Cx2eLaI5agtQTQvg4j+MrsbjgW1fQy /EiatxfElqGjS4Ws4vvPMfKQmWsPiZxQbAcSRGw= X-Received: by 2002:a4a:6505:: with SMTP id y5mr2149251ooc.67.1589127204521; Sun, 10 May 2020 09:13:24 -0700 (PDT) MIME-Version: 1.0 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> <9526fc07-cf21-03e8-1c68-acccc2941117@gmail.com> In-Reply-To: <9526fc07-cf21-03e8-1c68-acccc2941117@gmail.com> From: Nicolai Kraus Date: Sun, 10 May 2020 17:13:13 +0100 Message-ID: Subject: Re: [HoTT] Identity versus equality To: Michael Shulman Cc: Thorsten Altenkirch , Jon Sterling , "'Martin Escardo' via Homotopy Type Theory" Content-Type: multipart/alternative; boundary="000000000000874a1a05a54d8263" --000000000000874a1a05a54d8263 Content-Type: text/plain; charset="UTF-8" I have to correct what I said an hour ago (thanks, Mike). We don't know whether "exo-Nat is cofibrant" implies that exo-limits of towers are fibrant. (And probably it doesn't.) In other words, we don't know the connection between axioms (A2) and (A3) in arXiv:1705.03307. -- Nicolai On Sun, May 10, 2020 at 4:23 PM Nicolai Kraus wrote: > 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 > . > > --000000000000874a1a05a54d8263 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I have to correct what I said an hour ago (thanks, Mi= ke). We don't know whether "exo-Nat is cofibrant" implies tha= t exo-limits of towers are fibrant. (And probably it doesn't.)
In other words, we don't know the connection between axioms (A2) and = (A3) in=C2=A0arXiv:1705.03307.
=C2=A0-- Nicolai

On Sun, May 10, 20= 20 at 4:23 PM Nicolai Kraus <nico= la...@gmail.com> wrote:
Yes, I think that is one main motivation for this axiom (tha= t 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 t= wo
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-limit= s of
> towers of fibrations are fibrant?=C2=A0 That's another useful axio= m 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 <nicola...@gmail.com> 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 woul= d want this coinductive type. But this is just a guess.
>> -- Nicolai
>>
>> On Sun, May 10, 2020 at 3:35 PM Michael Shulman <shu...@sandiego.edu> wrot= e:
>>> Many or all coinductive types can be constructed, at least up = to
>>> equivalence, using Pi-types and (some kind of) Nat.=C2=A0 Is t= here 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 <nicola...@gmail.com> wr= ote:
>>>> On 10/05/2020 15:01, Michael Shulman wrote:
>>>>> On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch >>>>> <Thorsten....@nottingham.ac.uk> wrote:
>>>>>> Defining simplicial types isn't entirely strai= ghtforward (as you know I suppose), because Delta is not directed. We can d= o 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.=C2= =A0 I assume the
>>>>> point you're making is that we don't have a (f= ibrant) *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 Thors= ten was
>>>> talking about the direct replacement construction in Chris= tian's and my
>>>> abstract arXiv:1704.04543. With the assumption "exo-N= at is cofibrant",
>>>> this gives us a fibrant type that one could call "sim= plicial 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 N= at 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 preserv= e fibrancy.=C2=A0 We
>>>>> don't know how to model "exo-Nat is fibrant&q= uot; in all higher toposes,
>>>>> but it's easy to interpret "exo-Nat is cofibr= ant" 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 "eng= ineering level"
>>>> that was discussed earlier in this thread. Allowing coindu= ctive types
>>>> with exo-Nat as an index makes it possible to use your pap= er (Higher
>>>> Stucture Identity Principle, arXiv:2004.06572) and get a c= onstruction 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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBr0Zh-uLfEZCXUap= K5KHFDxkzxyvLW22zyjmrB8KmWtYQ%40mail.gmail.com.

--000000000000874a1a05a54d8263--