Evan Cavallo

I think in some sense one would rather not ask these questions; you might like to take the position that you should never talk about univalence without funext (or you should never go without funext, period). In a way I think it's a point against HoTT that it doesn't discourage us from asking these questions. You would never be tempted to think about this in cubical type theory, for example, because funext is built in at a much more fundamental level than univalence is. I've certainly come out of this feeling like we still have a lot to understand about foundations. Jonas and I have a similar taste in weird models and weird axioms and we had a lot of fun working on this. We're also eager to think about type theories with funext from now on :) Anyway, Jonas will be presenting this at MFPS this summer! (2/2)

@carloangiuli@mathstodon.xyz In the paper, we just do this for cartesian cubical type theory + reversals. For De Morgan cubical type theory, we would need to start from a good model of Dedekind cubical type theory. Christian's model that he claimed at TYPES 2025 will do, but since it's not a straight ABCHFL model there's a little extra bookkeeping to check, and since that model isn't written down yet we couldn't really fit that into this paper. Probably it will appear in whatever he writes for his model (and I will harass him to make it happen). But I would say the ideas are all there for a good model of DeM now.

@carloangiuli@mathstodon.xyz technically Thierry and I are GU and Christian is Chalmers! (though admin insists we list both on everything so they can juice their publication numbers)