Σ-closed reflective subuniverses
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-05-09.
Last modified on 2023-09-15.
module orthogonal-factorization-systems.sigma-closed-reflective-subuniverses where
Imports
open import foundation.dependent-pair-types open import foundation.sigma-closed-subuniverses open import foundation.universe-levels open import orthogonal-factorization-systems.reflective-subuniverses
Idea
A reflective subuniverse is Σ-closed if it is closed under the formation of Σ-types.
Definition
is-closed-under-Σ-reflective-subuniverse : {l lP : Level} → reflective-subuniverse l lP → UU (lsuc l ⊔ lP) is-closed-under-Σ-reflective-subuniverse (P , _) = is-closed-under-Σ-subuniverse P closed-under-Σ-reflective-subuniverse : (l lP : Level) → UU (lsuc l ⊔ lsuc lP) closed-under-Σ-reflective-subuniverse l lP = Σ ( reflective-subuniverse l lP) ( is-closed-under-Σ-reflective-subuniverse)
See also
The equivalent notions of
- Higher modalities
- Uniquely eliminating modalities
- Stable orthogonal factorization systems
- Σ-closed reflective modalities
References
- Egbert Rijke, Michael Shulman, Bas Spitters, Modalities in homotopy type theory, Logical Methods in Computer Science, Volume 16, Issue 1, 2020 (arXiv:1706.07526, doi:10.23638)
Recent changes
- 2023-09-15. Egbert Rijke. update contributors, remove unused imports (#772).
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-05-09. Fredrik Bakke and Egbert Rijke. Some half-finished additions to modalities (#606).