From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a02:a1d8:: with SMTP id o24mr2672999jah.88.1589134716527; Sun, 10 May 2020 11:18:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a92:ce4c:: with SMTP id a12ls2694068ilr.8.gmail; Sun, 10 May 2020 11:18:35 -0700 (PDT) X-Received: by 2002:a92:cac7:: with SMTP id m7mr13423323ilq.6.1589134714934; Sun, 10 May 2020 11:18:34 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589134714; cv=none; d=google.com; s=arc-20160816; b=kfjfscWi2TKbsX6bo1t5fAWz27C51cOp8qvzgjyaqULZLIOmiVjqNB1Ve5vW6BjRNP EzpQ18uyllQn7oVSmmecyBUVKH6VUNLYC+TvcXtBleyKdjIk2DJILmQ+YY3tkkHF+4PV xObil3+ulBWrcb6QvWg4sPf8lZ6VcYnVbnZwkgAptzNKWXyfeMjJGuP/WjAxDGYCkK6O ZuEfC2Nrm6SORfRUf9SiHrJ/bkEPnjgRMGLS7+yyjZ1Rwu0Qwc/GNpgNb4JHGxBRGI8h Dl23dABktFNa8Mj+n+nSkhMUuZagqBYAhDeyH2TFNSuYM9IDh6J8s1mFUGLE9RIZXsId s6+g== 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=2YYjRSSRvgQUbKPVt+tZH+xWD+o4NLh2eu4OFvlcPt8=; b=Ajjsp3ceGFJox4Pa9pQ7bwHuFHhGMRTzNCAYVW2Z/YjnROArDIfvItHS776ONOCmpU nzsb2Bce0SFGk0j0RCTEbDYNd7ZFrguuMs73TrkiHwEWDUCX61POJqFe9jAogAYT2k1/ 1D0HqByQnwfmRpnsepGPvAv+aYdE1vuP2ajfMpovvqyuQGGJ+Yb6o7KflrnEOaP928iz x4oB+MgT4UcBP1M3IFRnJOoW+Kp4FqJaXG9sgEsquuYIk5Qyv1PyEYGPaHeACu7kylNZ GBIPvdUJXvSvRCS0oONZT4g0P6QYQjGYSSmTqUtvmOBhrm3uGkZLfrExULaYhTzyUL1d 209Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Gr7gqnHO; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::333 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-ot1-x333.google.com (mail-ot1-x333.google.com. [2607:f8b0:4864:20::333]) by gmr-mx.google.com with ESMTPS id h14si496337iol.1.2020.05.10.11.18.34 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 11:18:34 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::333 as permitted sender) client-ip=2607:f8b0:4864:20::333; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=Gr7gqnHO; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::333 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-ot1-x333.google.com with SMTP id z17so5757299oto.4 for ; Sun, 10 May 2020 11:18:34 -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=2YYjRSSRvgQUbKPVt+tZH+xWD+o4NLh2eu4OFvlcPt8=; b=Gr7gqnHOXr65LSlbpz59JNYdm4eQHMovgYWwHVP8aF3N5PXnbXSQVYop6ybDheMlSE x6TabGj4JB2bSKNfOPVaid4u9gMN5iYPTbjbr5V8WtNaHxjZzOwJPEqFbQy2u/p0bSRq txTavgWeRjnVCstHYz0uAWc8p9N0Vo2Hf8bWYKi7piAkb2KbcnA0PgGhcCKb5eWb7kTe JS+xsGafLQ6Kwgx3D585btklQG/MopQVpYKymicqRazSO8b7hmbpY53rlnEcZn6sS59k +cXzYUgTUz/dcE2cUXaCCauVR7EYRfNzNF9MmdsRZaSHFGrs+eikpODkX95597J49niA hx7Q== X-Gm-Message-State: AGi0PuZNR0/r5ur5g6+ZxNAyuhD/WGpIPfVh20Jov5ibmz8eYi/dJaib kdGshwXlzGCpfuPLOgiMU6GwWO+0kYceU7tRyI44j2jxXjOR2w== X-Received: by 2002:a9d:6303:: with SMTP id q3mr9882230otk.14.1589134714594; Sun, 10 May 2020 11:18:34 -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: From: Nicolai Kraus Date: Sun, 10 May 2020 19:18:23 +0100 Message-ID: Subject: Re: [HoTT] Identity versus equality To: Michael Shulman Cc: "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary="00000000000029ebe605a54f4200" --00000000000029ebe605a54f4200 Content-Type: text/plain; charset="UTF-8" Yes, this is nice. We should add it to the next revision of the paper (arXiv:1705.03307). On Sun, May 10, 2020 at 5:29 PM Michael Shulman wrote: > Okay. But the implication works in the other way, doesn't it? A > product indexed by exo-Nat is the exo-limit of a tower of finite > products. So maybe the tower axiom is the best one. > > On Sun, May 10, 2020 at 9:13 AM Nicolai Kraus > wrote: > > > > 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 < > 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 would > 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> 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 < > nicola...@gmail.com> 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 > . > >> > > -- > > 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%2BAZBBrJF92OezfqYyh9vy-JQNesC8%2BpacAPPrq-xDZN5Y6qNQ%40mail.gmail.com > . > > -- > 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/CAOvivQz_JCE8QPTomY7ViOX%3DPgzZ_5aM3t9fx613jyfuOAUtvA%40mail.gmail.com > . > --00000000000029ebe605a54f4200 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Yes, this is nice. We should add it to the next revision o= f the paper (arXiv:1705.03307).

On Sun, May 10, 2020 at 5:29 PM Michael Shul= man <shu...@sandiego.edu> = wrote:
Okay.=C2= =A0 But the implication works in the other way, doesn't it?=C2=A0 A
product indexed by exo-Nat is the exo-limit of a tower of finite
products.=C2=A0 So maybe the tower axiom is the best one.

On Sun, May 10, 2020 at 9:13 AM Nicolai Kraus <nicola...@gmail.com> wrote:
>
> 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 t= owers are fibrant. (And probably it doesn't.)
> In other words, we don't know the connection between axioms (A2) a= nd (A3) in arXiv:1705.03307.
>=C2=A0 -- Nicolai
>
> On Sun, May 10, 2020 at 4:23 PM Nicolai Kraus <nicola...@gmail.com> wrote:
>>
>> Yes, I think that is one main motivation for this axiom (that you&= #39;ve
>> suggested in this form :-) and I also believe that it was Vladimir= 's
>> main motivation for his axiom "exo-Nat is fibrant". I th= ink 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?=C2=A0 That's another us= eful axiom that
>> > holds in models and might make it easier to construct coinduc= tive
>> > types with judgmental computation rules.
>> >
>> > On Sun, May 10, 2020 at 7:52 AM Nicolai Kraus <nicola...@gmail.com> w= rote:
>> >> I would guess that "exo-Nat is cofibrant" justi= fies the coinductive type in question, but not its judgmental computation r= ules. 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 <shu...@sandiego.edu= > wrote:
>> >>> Many or all coinductive types can be constructed, at = least up to
>> >>> equivalence, using Pi-types and (some kind of) Nat.= =C2=A0 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 <nicola...@gmail.com> wrote:
>> >>>> On 10/05/2020 15:01, Michael Shulman wrote:
>> >>>>> On Sun, May 10, 2020 at 4:46 AM Thorsten Alte= nkirch
>> >>>>> <
Thorsten....@nottingham.ac.uk> wrote:
>> >>>>>> Defining simplicial types isn't entir= ely 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 t= ype
>> >>>>> We can certainly *talk* about simplicial type= s 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 (fibrant) *type of*
>> >>>>> simplicial types, whereas we do have a fibran= t type of semisimplicial
>> >>>>> types (under appropriate axioms)?
>> >>>> Judging from the rest of his message, I believe t= hat Thorsten was
>> >>>> talking about the direct replacement construction= in Christian's and my
>> >>>> abstract arXiv:1704.04543. With the assumption &q= uot;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 encodin= g. If we decide to use such
>> >>>> encodings, I fear we may lose the main advantage = that the "axiomatic"
>> >>>> representations in HoTT have, namely avoiding enc= odings. (I mean the
>> >>>> "main advantage" of HoTT compared to tr= aditional 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 her= e is that exo-Nat is
>> >>>>> *cofibrant*, i.e. Pi-types with domain exo-Na= t preserve fibrancy.=C2=A0 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 e= xternally-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. Allowi= ng coinductive types
>> >>>> with exo-Nat as an index makes it possible to use= your paper (Higher
>> >>>> Stucture Identity Principle, arXiv:2004.06572) an= d 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 t= he 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-u= LfEZCXUapK5KHFDxkzxyvLW22zyjmrB8KmWtYQ%40mail.gmail.com.
>>
> --
> You received this message because you are subscribed to the Google Gro= ups "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 http= s://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBrJF92OezfqYyh9vy-= JQNesC8%2BpacAPPrq-xDZN5Y6qNQ%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyT...@googlegroups.com.
To view this discussion on the web visit https://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQz_JCE8QPTomY7ViOX%3DPgzZ_5= aM3t9fx613jyfuOAUtvA%40mail.gmail.com.
--00000000000029ebe605a54f4200--