Characterizations of modalities and lex modalities

TL;DR

This paper provides new characterizations of various types of modalities in homotopy type theory, clarifying their properties and relationships through conditions on associated classes of maps.

Contribution

It introduces novel characterizations of modalities, lex modalities, and cotopological modalities in homotopy type theory, linking them to classes of maps and their orthogonal complements.

Findings

Characterizations of $L$-modalities and related concepts.

Conditions involving $L$-étale maps, $L$-equivalences, and $L$-local maps.

Examples demonstrating strict inclusions among classes of maps.

Abstract

A reflective subuniverse in homotopy type theory is an internal version of the notion of a localization in topology or in the theory of $\infty$-categories. Working in homotopy type theory, we give new characterizations of the following conditions on a reflective subuniverse $L$: (1) the associated subuniverse $L'$ of $L$-separated types is a modality; (2) $L$ is a modality; (3) $L$ is a lex modality; and (4) $L$ is a cotopological modality. In each case, we give several necessary and sufficient conditions. Our characterizations involve various families of maps associated to $L$, such as the $L$-\'etale maps, the $L$-equivalences, the $L$-local maps, the $L$-connected maps, the unit maps $\eta_X$, and their left and/or right orthogonal complements. More generally, our main theorem gives an overview of how all of these classes related to each other. We also give examples that show that all of the inclusions we describe between these classes of maps can be strict.