This paper proves that a directed version of Voevodsky’s univalence axiom holds for a broad semantic setting: simplicial objects in any infinity-topos. In plain terms, the authors show that in the right universe of types, the “hom” between two types (the ways to go from one object to another) is equivalent to the ordinary notion of functions between those types. They also prove a stronger, higher-dimensional version that compares coherent composites of arrows with composable sequences of functions.

The work focuses on the covariant universe given by the universal left fibration. A left fibration is a family of spaces (also called infinity-groupoids) that vary covariantly over a base; intuitively its fibres are the possible values over each point of the base and they change in a forward-directed way along arrows. The authors construct a universal left fibration that classifies all small left fibrations inside an infinity-topos, and they build an internal category over that universe whose object of arrows they call Fun1. Their main theorem identifies the hom-types coming from this universe with the function-types encoded by Fun1.

How they prove it, at a high level, is a mix of model-categorical constructions and a reduction trick. They use known presentations of infinity-topoi by model categories (following work of Lurie, Rezk, and Shulman) to construct the universal left fibration as a morphism π: eUcov → Ucov. Then, using the technique of weighted limits, they reduce the general statement for simplicial objects in any infinity-topos to concrete calculations with simplicial sets. This reduction lets them verify a pointwise equivalence of simplicial objects that is natural up to homotopy, and then lift that equivalence back to the internal setting.

Why this matters: univalence is a central principle in homotopy type theory because it links identity of types to equivalences between them. A directed univalence axiom plays the same foundational role for a version of type theory aimed at describing infinity-categories rather than infinity-groupoids. By verifying directed univalence in this semantic setting, the authors give a solid semantic foundation for simplicial type theory’s covariant universe. The higher-dimensional form of the result also shows that coherent compositions of arrows in the universal left fibration correspond to ordinary composable sequences of functions, which clarifies how composition is represented internally.