Bartosz MilewskiAnother blog post in the HoTT series.
https://bartoszmilewski.com/2026/03/10/the-axiom-of-univalence/
https://bartoszmilewski.com/2026/03/10/the-axiom-of-univalence/
Tom de Jong@BartoszMilewski Maybe you already know this, but what you wrote is not quite the univalence axiom, see e.g. Section 3 of https://drops.dagstuhl.de/storage/00lipics/lipics-vol104-types2017/LIPIcs.TYPES.2017.6/LIPIcs.TYPES.2017.6.pdf
@de_Jong_Tom
What am I missing?
It looks like my definition (which is Axiom 2.10.3 in the HoTT book) is Def 3.2 in the paper you're citing.
I used an alternative definition of equivalence: 2.4.10 in the HoTT book.
@BartoszMilewski You're postulating that there is *some* equivalence, not that the canonical map idtoeqv (that sends refl to the identity equivalence) is an equivalence. So what you have is Def 3.3 ("naive univalence") in that paper. The difference between the two is precisely Theorem 3.5.
Aside: Note that the "proper" univalence axiom is a property, i.e. the type that expresses it is a proposition, while the naive univalence axiom is not (I think — at least not obviously).
@de_Jong_Tom
I see. The word "hence" is very meaningful here. To invert this you need the computation rule.
I see. The word "hence" is very meaningful here. To invert this you need the computation rule.
