Characterizations of modalities and lex modalities |
| |
Authors: | J Daniel Christensen Egbert Rijke |
| |
Institution: | 1. Department of Mathematics, University of Western Ontario, London, Ontario, Canada;2. Department of Mathematics, University of Ljubljana, Jadranska Ulica 21, 1000 Ljubljana, Slovenia;1. Universidad de Cádiz, Puerto Real, Cádiz, Spain;2. CMCC, Universidade Federal do ABC, Santo André, Brazil;3. CMUP, Faculdade de Ciências, Universidade do Porto, Porto, Portugal;4. Moscow Center for Fundamental and Applied Mathematics, Moscow, Russia;5. Departamento de Matemática, Universidade Federal de Santa Catarina, Florianópolis, Brazil;6. Departamento de Matemática, Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa, Caparica, Portugal;7. Saint Petersburg University, Saint Petersburg, Russia |
| |
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 ∞-categories. Working in homotopy type theory, we give new characterizations of the following conditions on a reflective subuniverse L: (1) the associated subuniverse 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-étale maps, the L-equivalences, the L-local maps, the L-connected maps, the unit maps , 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. |
| |
Keywords: | Reflective subuniverse Localization Modality Lex modality Factorization system Homotopy type theory |
本文献已被 ScienceDirect 等数据库收录! |
|