Σ-closed reflective subuniverses

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-09.
Last modified on 2024-03-12.

module orthogonal-factorization-systems.sigma-closed-reflective-subuniverses where

open import foundation.dependent-pair-types
open import foundation.sigma-closed-subuniverses
open import foundation.universe-levels

open import orthogonal-factorization-systems.reflective-subuniverses

Idea

A reflective subuniverse is Σ-closed if it is closed under the formation of Σ-types.

Definition

is-closed-under-Σ-reflective-subuniverse :
  {l lP : Level} → reflective-subuniverse l lP → UU (lsuc l ⊔ lP)
is-closed-under-Σ-reflective-subuniverse (P , _) =
  is-closed-under-Σ-subuniverse P

closed-under-Σ-reflective-subuniverse :
  (l lP : Level) → UU (lsuc l ⊔ lsuc lP)
closed-under-Σ-reflective-subuniverse l lP =
  Σ ( reflective-subuniverse l lP)
    ( is-closed-under-Σ-reflective-subuniverse)

See also

The equivalent notions of

• Higher modalities
• Uniquely eliminating modalities
• Stable orthogonal factorization systems
• Σ-closed reflective modalities

References

[RSS20]

Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, 01 2020. URL: https://lmcs.episciences.org/6015, arXiv:1706.07526, doi:10.23638/LMCS-16(1:2)2020.

Recent changes

• 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
• 2023-11-01. Fredrik Bakke. Opposite categories, gaunt categories, replete subprecategories, large Yoneda, and miscellaneous additions (#880).
• 2023-09-15. Egbert Rijke. update contributors, remove unused imports (#772).
• 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
• 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).