Stable orthogonal factorization systems

module orthogonal-factorization-systems.stable-orthogonal-factorization-systems where

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 is an orthogonal factorization system whose left class is stable under pullbacks.

The right class of an orthogonal factorization system 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 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)