The Natural Display Topos of Coalgebras

A classical result of topos theory holds that the category of coalgebras for a Cartesian comonad on a topos is again a topos (Kock and Wraith, 1971). 

It is natural to refine this result to a topos-theoretic setting that includes universes. To this end, we introduce the notions of natural display topos and natural Cartesian display comonad, and show that the natural model of coalgebras for a natural Cartesian display comonad on a natural display topos is again a natural display topos. As an application, this result extends the approach to universes of Hofmann and Streicher (1997) from presheaf toposes to sheaf toposes with enough points. 

Whereas natural display toposes provide a categorical semantics for a form of extensional Martin-Löf type theory, we also prove our main result in the more general setting of natural typoses, which encompasses models of intensional Martin-Löf type theory. 

A natural Cartesian display comonad on a natural typos may also be used as a model for dependent type theory with an S4 box operator, or comonadic modality, as introduced by Nanevski et al. (2008). Modal contexts, which have been regarded as tricky to handle semantically, are interpreted as contexts of the natural typos of coalgebras. We sketch an interpretation within this approach. 

As part of the framework in which the above takes place, we introduce a refinement of the notion of natural model (see Awodey, 2018), which is (strictly 2- )equivalent to the notion of full, split comprehension category (see Jacobs, 1993), rather than the notion of category with attributes (Cartmell 1978).