Strict universes for Grothendieck topoi
Daniel Gratzer, Michael Shulman, Jonathan Sterling

TL;DR
This paper constructs cumulative universe hierarchies with the realignment property in all Grothendieck topoi, enabling direct interpretations of Martin-Löf type theory and extending synthetic methods in type theory semantics.
Contribution
It introduces a slight modification of Shulman's argument to build cumulative universes with the realignment property in any Grothendieck topos, broadening the applicability of synthetic methods.
Findings
Cumulative universe hierarchies with realignment property are constructed in all Grothendieck topoi.
Direct-style interpretations of Martin-Löf type theory with cumulative universes are possible.
Extension of synthetic methods in type theory semantics to all Grothendieck topoi.
Abstract
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 the presheaf universes that plays a critical role in models of univalent type theory as well as synthetic Tait computability, a recent technique to establish syntactic properties of type theories and programming languages. In the context of multiple universes, the realignment property also implies a coherent choice of codes for connectives at each universe level, thereby interpreting the cumulativity laws present in popular formulations of Martin-L\"of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
