Re: [HoTT] Identity versus equality

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

Dear Thomas,

    I mostly agree with what Jon said. I also think that intensional type
    theory within an extensional type theory (it is 2 levels and not 3) is
    an attractive system for cubical type theory.

That seems to be putting the cart before the horse. HoTT is the theory I want to work in, the strict layer is only there to do some internalized metatheory.

    In the simplicial case this is a bit more problematic since the
    filling conditions for Kan complexes involve classical existential
    quantification and as shown by Thierry et.al. this is important!

I think we have two discussions here: one is about simplicial sets which is about the reduction of HoTT to set level structures and the other is about (semi-)simplicial types which is about modelling higher structures within HoTT.

The classical assumptions in the filling conditions for Kan complexes can be avoided as was shown by Gambino and Sattler:
https://arxiv.org/abs/1510.00669
who develop a theory of uniform fibrations that captures both cubical and simplicial sets. This means we can model Pi-types using uniform simplicial sets. However, it is not clear how to interpret a univalent universe in uniform simplicial sets. It is possible to do this in uniform cubical sets due to the fact that the interval is a tiny object.

    That the extensional level is just formulated using J and K is a
    possibility. It has to be seen in practice how far it goes.

You need K on the strict level, because that is exactly the point that you don’t need to care about coherences anymore. Btw, I think calling it "extensional level" is a misnomer because actually the fibrant layer is more extensional than the strict one because it is univalent. 

So for example if you define semi-simplicial types in a 2-level type theory it is essential that you have K.

Cheers,
Thorsten




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.