Hofmann and Streicher famously showed how to lift Grothendieck universes into presheaf topoi, and Streicher has extended their result to the case of sheaf topoi by sheafification. In parallel, van den Berg and Moerdijk have shown in the context of algebraic set theory that similar constructions continue to apply even in weaker metatheories. Unfortunately, sheafification seems not to preserve an important realignment property enjoyed by presheaf universes that plays a critical role in models of univalent type theory as well as synthetic Tait computability. When multiple universes are present, realignment also implies a coherent interpretation of connectives across all universes that justifies the cumulativity laws present in popular formulations of Martin-Löf type theory.
We observe that a slight adjustment to an argument of Shulman lifts a well-behaved cumulative universe hierarchy in the category of sets to a cumulative universe hierarchy satisfying the realignment property at every level in any Grothendieck topos. Hence one has direct interpretations of Martin-Löf type theory with cumulative universes into all Grothendieck topoi. A further implication is to extend the reach of recent synthetic methods in the semantics of cubical type theory and the syntactic metatheory of type theory and programming languages to all Grothendieck topoi.
Keywords: homotopy type theory, topos theory, univalence axiom
2020 MSC: 55U35, 18G55, 03G30
Theory and Applications of Categories, Vol. 45, 2026, No. 30, pp 1227-1279.
Published 2026-05-20.
TAC Home