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 2026-03-06.

Instances of higher modalities

Modules in the orthogonal factorization systems namespace

module orthogonal-factorization-systems where

open import orthogonal-factorization-systems.anodyne-maps public
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.connected-maps-at-subuniverses public
open import orthogonal-factorization-systems.connected-maps-at-subuniverses-over-type public
open import orthogonal-factorization-systems.connected-types-at-subuniverses public
open import orthogonal-factorization-systems.continuation-modalities public
open import orthogonal-factorization-systems.coproducts-null-types 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.equality-extensions-dependent-maps public
open import orthogonal-factorization-systems.equality-extensions-maps public
open import orthogonal-factorization-systems.equivalences-at-subuniverses public
open import orthogonal-factorization-systems.extensions-dependent-maps 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.postcomposition-extensions-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.weakly-anodyne-maps 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

• 2026-03-06. Fredrik Bakke. Oracle modalities (#1879).
• 2026-02-26. Fredrik Bakke. Coproducts of null types (#1868).
• 2025-11-12. Fredrik Bakke. Subuniverse equivalences and connected maps (#1669).
• 2025-11-12. Fredrik Bakke. chore: Rename extension to extension-map and lift to lift-map (#1706).
• 2025-11-12. Fredrik Bakke. Refactor extensions of maps (#1695).