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 > . > >