Re: [HoTT] Identity versus equality

[Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>]

On 10/05/2020, 15:06, "Michael Shulman" <shu...@sandiego.edu> 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)?

Yes, by talking about I meant within HoTT. I mean we want to understand them as structures not just as some set-level encoding. 

Also I find the Kan-condition more natural in HoTT because we just need to state an equivalence. On the level of set-level Mathematics we either hide the witness or we need to introduce uniformity conditions. 

I also don't think it is an issue that Delta is not direct because Delta is based on the hack to build identities into the framework but obtain composition via the Kan condition. Hence I think we should represent identities in the same way as composition.

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




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.