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 2024-11-05.
Examples of higher modalities
| Modality | File |
|---|---|
| The closed modalities | orthogonal-factorization-systems.closed-modalities |
| Continuation modalities | orthogonal-factorization-systems.continuation-modalities |
| The double negation modality | foundation.double-negation-modality |
| The identity modality | orthogonal-factorization-systems.identity-modality |
| The open modalities | orthogonal-factorization-systems.open-modalities |
| Raising universe level modalities | orthogonal-factorization-systems.raise-modalities |
| The truncation modalities | foundation.truncation-modalities |
| The zero modality | orthogonal-factorization-systems.zero-modality |
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-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.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.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-pullback-hom 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-of-maps public open import orthogonal-factorization-systems.local-families-of-types 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-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-modalities public open import orthogonal-factorization-systems.reflective-subuniverses public open import orthogonal-factorization-systems.regular-cd-structures 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.types-colocal-at-maps public open import orthogonal-factorization-systems.uniquely-eliminating-modalities 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
- 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).
- 2024-09-06. Fredrik Bakke. Colocal types (#1089).
- 2024-06-04. Fredrik Bakke. Fiberwise orthogonal maps and closure properties of the right class (#1152).