Stable orthogonal factorization systems
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2023-05-09.
Last modified on 2023-06-28.
module orthogonal-factorization-systems.stable-orthogonal-factorization-systems where
Imports
open import foundation.universe-levels open import orthogonal-factorization-systems.function-classes open import orthogonal-factorization-systems.orthogonal-factorization-systems
Idea
A stable orthogonal factorization system, or stable factorization system for short, is an orthogonal factorization system whose left class is stable under pullbacks. The right class of an orthogonal factorization system, however, is always stable under pullbacks.
Definition
is-stable-orthogonal-factorization-system : {l1 lL lR : Level} (l2 : Level) → orthogonal-factorization-system l1 lL lR → UU (lsuc l1 ⊔ lL ⊔ lsuc l2) is-stable-orthogonal-factorization-system l2 OFS = is-pullback-stable-function-class ( l2) ( left-class-orthogonal-factorization-system OFS)
See also
The equivalent notions of
- Higher modalities
- Uniquely eliminating modalities
- Σ-closed reflective modalities
- Σ-closed reflective subuniverses
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-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
- 2023-05-09. Fredrik Bakke and Egbert Rijke. Some half-finished additions to modalities (#606).