Projective Presentations of Lex Modalities

TL;DR

This paper introduces presentations of topological modalities in homotopy type theory, enabling internal sheaf conditions and cohomology comparisons across universes, with applications to algebraic geometry and higher category theory.

Contribution

It defines a new internalization of Grothendieck topologies in homotopy type theory, providing computational tools and stability results for cohomology across different topologies.

Findings

Presentations of modalities can determine subuniverse membership via internal sheaf conditions.

Assuming the axiom of choice, powerful computational tools for modalities are developed.

Cohomology of certain algebraic structures remains stable across different topologies.

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, \'etale and fppf toposes.