Thanks to everyone who replied!
Just for the reference since Christian's email went only to me: there is a remark in the paper that states it is possible to make the theory extensional, so it appears 2LTT is exactly the type theory I was looking for.
Best,
Kristina
See axiom (A5) in Section 2.4:
(A5) We can ask that the outer level validates the equality reflection rule, i.e. forms a model of extensional type theory. This is the case in all the example models we are interested in.
Equality reflection is supported in presheaf models, which justify conservativity over HoTT. The main problem with equality reflection is syntactical, in that we don't have good proof assistant support for it...
--
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 HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/60639a49-a1c6-0cfd-0bdf-65ad45b14e24%40gmail.com.