Σ-closed reflective subuniverses

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-05-09.
Last modified on 2023-09-15.

module orthogonal-factorization-systems.sigma-closed-reflective-subuniverses where
Imports
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

References

  • Egbert Rijke, Michael Shulman, Bas Spitters, Modalities in homotopy type theory, Logical Methods in Computer Science, Volume 16, Issue 1, 2020 (arXiv:1706.07526, doi:10.23638)

Recent changes