Stable orthogonal factorization systems

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-09.
Last modified on 2024-03-12.

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} →
  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

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.

Recent changes