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
| Modality | File |
|---|---|
| The closed modalities | orthogonal-factorization-systems.closed-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 |
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
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
- 2023-05-09. Fredrik Bakke and Egbert Rijke. Some half-finished additions to modalities (#606).
- 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).