Stratified Toposes

TL;DR

This paper introduces stratified toposes, a hierarchy-based extension of topos theory that models the calculus of constructions and refines existing coalgebra constructions, providing new foundational insights.

Contribution

It strengthens Streicher's axioms to define stratified toposes and demonstrates their application through a refined coalgebra construction on stratified toposes.

Findings

Refined the axioms of Streicher for stratified toposes

Constructed the stratified topos of coalgebras for a stratified Cartesian comonad

Identified conditions for lifting monomorphisms and dense subcategories to coalgebras

Abstract

We introduce stratified toposes, which are toposes that are stratified by a suitable hierarchy of universes. The term `stratified topos' recalls the notion of stratified pseudotopos of Moerdijk and Palmgren (2002). However, the details of our proposal are closer to that of Streicher (2005), with the foundational contribution being a strengthening of Streicher's axioms. As such, stratified toposes model the calculus of constructions. Key results about toposes can be refined to yield results about stratified toposes. As proof of concept, we construct what we call the stratified topos of coalgebras for a stratified Cartesian comonad on a stratified topos. This construction refines that of the topos of coalgebras for a Cartesian comonad on a topos. Coalgebra constructions in related settings were given by Warren (2007) and Zwanziger (2023). This coalgebra construction exposes conditions under which generic monomorphisms and dense subcategories can be lifted to coalgebras, which are extracted in the appendix.