Pointed Univalence

Voevodsky’s Univalence Axiom is perhaps the most fundamental logical principle introduced in the 21st century. A universe of (small) types satisfies the univalence axiom if, for any two types in that universe, their type of equalities (or identifications) is equivalent to the type of equivalences between them. Thus, for example, two logically equivalent propositions or bijective sets can be treated as equal, and hence substituted for each other in all contexts. While convenient and often assumed in informal mathematical practice, the univalence axiom requires formal justification. The first such justification comes from Voevodsky’s celebrated simplicial model [2]; the model that not only satisfies, but in fact inspired, the univalence axiom.

In [2], the goal is to build a single model of homotopy type theory (in simplicial sets), and when it comes to verifying univalence, the authors do just that: they translate the statement into a statement about simplicial sets and check it directly. In contrast, in [1], we make two further contributions to categorical univalent type theory. First, we provide a more general semantic treatment of univalence at the level of Voevodsky’s universe categories [5] by rephrasing the condition in a way that is easy to check across various models. We also aim to avoid using the internal language formulations which, while elegant, might occasionally conceal important details, possibly leading to incomplete arguments. Altogether, the upshot of our formulation is that, when verifying univalence in a universe category model, one does not need to work with syntax at all.

Interestingly, to arrive at a formulation of univalence that can be easily verified in a universe category, we actually give a stronger statement than the one commonly used and given in the HoTT Book [4], which brings us our second contribution. As mentioned before, univalence traditionally formulated by saying that a certain map from the identity type between two types in a universe to the type of equivalences between them is itself an equivalence. Our strengthening requires that the homotopy inverse of this map sends the identity equivalence to the reflexivity term. To differentiate the two, we call the version found in [4] book univalence and our new version pointed univalence, which is based on a lifting condition. While book univalence asks for a certain commutative square to admit a diagonal filler making only the lower triangle commute, pointed univalence requires that both resulting triangles commute. As such, pointed univalence is natural to verify in models coming from Quillen model categories, where fillers make both triangles commute. Furthermore, since maps from the left class to fibrations axiomatize pattern matching, our pointed univalence is also computationally desirable, as it justifies performing pattern matching on equivalences. Thus, we believe this strengthening constitutes a new notion of independent interest with strong semantic justification.

Our semantic study of pointed univalence includes studying closure properties of models under two fundamental constructions: Artin–Wraith gluing and inverse diagrams. For book univalence, these were verified in the seminal work of Shulman [3], and we provide the “pointed counterpart” of his results.