Projective Presentations of Lex Modalities

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.