Orthogonal factorization systems

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2023-02-06.
Last modified on 2023-09-11.

Examples of higher modalities

Files in the orthogonal factorization systems folder

module orthogonal-factorization-systems where

open import orthogonal-factorization-systems.closed-modalities public
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.identity-modality 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-families public
open import orthogonal-factorization-systems.local-maps public
open import orthogonal-factorization-systems.local-types public
open import orthogonal-factorization-systems.localizations-maps public
open import orthogonal-factorization-systems.localizations-subuniverses public
open import orthogonal-factorization-systems.locally-small-modal-operators 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.open-modalities 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.raise-modalities public
open import orthogonal-factorization-systems.reflective-modalities public
open import orthogonal-factorization-systems.reflective-subuniverses public
open import orthogonal-factorization-systems.separated-types public
open import orthogonal-factorization-systems.sigma-closed-modalities public
open import orthogonal-factorization-systems.sigma-closed-reflective-modalities 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
open import orthogonal-factorization-systems.zero-modality public

Recent changes