This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

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, 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} →
  orthogonal-factorization-system l1 lL lR → UU (lsuc l1 ⊔ lL)
is-stable-orthogonal-factorization-system OFS =
  is-pullback-stable-function-class
    ( left-class-orthogonal-factorization-system OFS)

See also

The equivalent notions of

• Higher modalities
• Uniquely eliminating modalities
• Σ-closed reflective modalities
• Σ-closed reflective subuniverses

References

[RSS20]

Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, 01 2020. URL: https://lmcs.episciences.org/6015, arXiv:1706.07526, doi:10.23638/LMCS-16(1:2)2020.