Re: [HoTT] Identity versus equality

[Michael Shulman <shu...@sandiego.edu>]

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 <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 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 <nicola...@gmail.com> 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
>> >>>>> <Thorsten....@nottingham.ac.uk> 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.