Projective Presentations of Lex Modalities
Mark Damuni Williams
TL;DR
The paper develops projective presentations of modalities in HoTT, embedding Grothendieck-topology-like covers and higher sheaf conditions into the internal logic. It introduces maximal and projective presentations, a local choice principle, and Kripke–Joyal semantics to transfer cohomology between universes via objects like $\bigcirc K(G,n)$. It then applies these tools to synthetic algebraic geometry and triangulated type theory, showing subcanonical presentations and cohomology stability across topoi, and providing explicit mechanisms for computing sheafifications and descent inside subuniverses. Overall, the work offers a constructive, computable framework for manipulating subuniverses, cohomology, and geometric reasoning within HoTT, with concrete implications for classifying topoi and synthetic geometry.
Abstract
Modalities in homotopy type theory are used to create and access subuniverses of a given type universe. These have significant applications throughout mathematics and computer science, and in particular can be used to create universes in which certain logical principles are true. We define presentations of topological modalities, which act as an internalisation of the notion of a Grothendieck topology. A specific presentation of a modality gives access to a surprising amount of computational information, such as explicit methods of determining membership of the subuniverse via internal sheaf conditions. Furthermore, assuming all terms of the presentation satisfy the axiom of choice, we are able to describe generic and powerful computational tools for modalities. This assumption is validated for presentations given by representables in presheaf categories. We deduce a local choice principle, and an internal reconstruction of Kripke-Joyal style reasoning. We use the local choice principle to show how to relate cohomology between universes, showing that a certain class of abelian groups has cohomolgoy stable between universes. We apply the methods to a prominent example, a type theory axiomatising the classifying topos of an algebraic theory, which specialises to give type theories for synthetic algebraic geometry and synthetic higher category theory. We apply the sheaf conditions to show that several presentations of interest are subcanonical, and apply the cohomology methods to show that quasi-coherent modules have cohomology stable between the Zariski, étale and fppf toposes.