Orthogonal factorization systems

Files in the orthogonal factorization systems folder

module orthogonal-factorization-systems where

open import orthogonal-factorization-systems.extensions-of-maps public
open import orthogonal-factorization-systems.factorization-operations public
open import orthogonal-factorization-systems.factorization-operations-function-classes public
open import orthogonal-factorization-systems.factorizations-of-maps public
open import orthogonal-factorization-systems.function-classes public
open import orthogonal-factorization-systems.higher-modalities public
open import orthogonal-factorization-systems.lifting-operations public
open import orthogonal-factorization-systems.lifting-squares public
open import orthogonal-factorization-systems.lifts-of-maps public
open import orthogonal-factorization-systems.local-types public
open import orthogonal-factorization-systems.mere-lifting-properties public
open import orthogonal-factorization-systems.modal-operators public
open import orthogonal-factorization-systems.null-types public
open import orthogonal-factorization-systems.orthogonal-factorization-systems public
open import orthogonal-factorization-systems.orthogonal-maps public
open import orthogonal-factorization-systems.pullback-hom public
open import orthogonal-factorization-systems.reflective-subuniverses public
open import orthogonal-factorization-systems.sigma-closed-reflective-subuniverses public
open import orthogonal-factorization-systems.stable-orthogonal-factorization-systems public
open import orthogonal-factorization-systems.uniquely-eliminating-modalities public
open import orthogonal-factorization-systems.wide-function-classes public