Orthogonal factorization systems

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Vojtěch Štěpančík and Raymond Baker.

Created on 2023-02-06.
Last modified on 2025-02-03.

Examples of higher modalities

Modules in the orthogonal factorization systems namespace

module orthogonal-factorization-systems where

open import orthogonal-factorization-systems.cd-structures public
open import orthogonal-factorization-systems.cellular-maps public
open import orthogonal-factorization-systems.closed-modalities public
open import orthogonal-factorization-systems.continuation-modalities public
open import orthogonal-factorization-systems.double-lifts-families-of-elements public
open import orthogonal-factorization-systems.double-negation-sheaves public
open import orthogonal-factorization-systems.extensions-double-lifts-families-of-elements public
open import orthogonal-factorization-systems.extensions-lifts-families-of-elements public
open import orthogonal-factorization-systems.extensions-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.factorization-operations-global-function-classes public
open import orthogonal-factorization-systems.factorizations-of-maps public
open import orthogonal-factorization-systems.factorizations-of-maps-function-classes public
open import orthogonal-factorization-systems.factorizations-of-maps-global-function-classes public
open import orthogonal-factorization-systems.families-of-types-local-at-maps public
open import orthogonal-factorization-systems.fiberwise-orthogonal-maps public
open import orthogonal-factorization-systems.function-classes public
open import orthogonal-factorization-systems.functoriality-higher-modalities public
open import orthogonal-factorization-systems.functoriality-localizations-at-global-subuniverses public
open import orthogonal-factorization-systems.functoriality-pullback-hom public
open import orthogonal-factorization-systems.functoriality-reflective-global-subuniverses public
open import orthogonal-factorization-systems.global-function-classes public
open import orthogonal-factorization-systems.higher-modalities public
open import orthogonal-factorization-systems.identity-modality public
open import orthogonal-factorization-systems.large-lawvere-tierney-topologies public
open import orthogonal-factorization-systems.lawvere-tierney-topologies public
open import orthogonal-factorization-systems.lifting-operations public
open import orthogonal-factorization-systems.lifting-structures-on-squares public
open import orthogonal-factorization-systems.lifts-families-of-elements public
open import orthogonal-factorization-systems.lifts-maps public
open import orthogonal-factorization-systems.localizations-at-global-subuniverses public
open import orthogonal-factorization-systems.localizations-at-maps public
open import orthogonal-factorization-systems.localizations-at-subuniverses public
open import orthogonal-factorization-systems.locally-small-modal-operators public
open import orthogonal-factorization-systems.maps-local-at-maps public
open import orthogonal-factorization-systems.mere-lifting-properties public
open import orthogonal-factorization-systems.modal-induction public
open import orthogonal-factorization-systems.modal-operators public
open import orthogonal-factorization-systems.modal-subuniverse-induction public
open import orthogonal-factorization-systems.null-families-of-types public
open import orthogonal-factorization-systems.null-maps 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.precomposition-lifts-families-of-elements public
open import orthogonal-factorization-systems.pullback-hom public
open import orthogonal-factorization-systems.raise-modalities public
open import orthogonal-factorization-systems.reflective-global-subuniverses public
open import orthogonal-factorization-systems.reflective-modalities public
open import orthogonal-factorization-systems.reflective-subuniverses public
open import orthogonal-factorization-systems.regular-cd-structures 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.types-colocal-at-maps public
open import orthogonal-factorization-systems.types-local-at-maps public
open import orthogonal-factorization-systems.types-separated-at-maps public
open import orthogonal-factorization-systems.uniquely-eliminating-modalities public
open import orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses public
open import orthogonal-factorization-systems.wide-function-classes public
open import orthogonal-factorization-systems.wide-global-function-classes public
open import orthogonal-factorization-systems.zero-modality public

Recent changes

• 2025-02-03. Fredrik Bakke. Reflective global subuniverses (#1228).
• 2024-11-19. Fredrik Bakke. Renamings and rewordings OFS (#1188).
• 2024-11-05. Fredrik Bakke and Egbert Rijke. Continuation modalities and Lawvere–Tierney topologies (#1157).
• 2024-10-15. Fredrik Bakke. Define double negation sheaves (#1198).
• 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).