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)

Something new on the arXiv from Jonas Höfer (@jhoefer@mathstodon.xyz) and I today: "Univalence without function extensionality" https://arxiv.org/abs/2605.00812

We look at a definition of "equivalence" where instead of asking for homotopies---i.e., pointwise equalities---between the inverses, we ask for equalities of functions. We call this a "categorical equivalence", because its the definition you arrive at if you think of the universe as a wild category. If you define univalence using categorical equivalence, i.e. if you ask for the universe to be a univalent wild category, it turns out you get an axiom that doesn't imply function extensionality! This has long been suspected (https://mathoverflow.net/questions/134449/equivalent-form-of-the-univalence-axiom), but we prove it with a countermodel based on Von Glehn's polynomial construction. This is a construction on models whose outputs always refute function extensionality, but it turns out it carries through some amount of univalence from the base model.

We also show that the canonical map from categorical equivalences to equivalences is a equivalence if and only if function extensionality holds. This is a sharpening of Voevodsky's classic result that univalence implies function extensionality in the universe, and the proof uses the same ideas. To me this is a kind of answer to the old question of what is really going on in Voevodsky's proof, and whether the implication from univalence to funext is really fundamental or just an "accident".

(1/2)

RE: @ecavallo@mathstodon.xyz

You can look forward to type theory is weird content at MFPS!

@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)

"The equivariant model structure on cartesian cubical sets" is published! https://doi.org/10.1016/j.aim.2026.110965

The arXiv version will be updated with the post-review changes shortly :)

You can look forward to cubical content at LICS!

papers are too long