The Natural Display Topos of Coalgebras

TL;DR

This paper extends classical topos-theoretic results to a setting involving natural display toposes and comonads, providing a categorical semantics for various forms of Martin-Löf type theory and modal dependent type theories.

Contribution

It introduces natural display toposes and natural Cartesian display comonads, extending topos-theoretic coalgebra results to models of extensional and intensional type theories with modalities.

Findings

Natural display toposes are closed under coalgebra constructions.

The framework models extensional and intensional Martin-Löf type theories.

Provides semantics for dependent type theories with S4 modal operators.

Abstract

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\"of type theory, we also prove our main result in the more general setting of natural typoses, which encompasses models of intensional Martin-L\"of 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).