Σ-closed reflective subuniverses

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

open import foundation.dependent-pair-types
open import foundation.functions
open import foundation.propositions
open import foundation.universe-levels

open import orthogonal-factorization-systems.modal-operators
open import orthogonal-factorization-systems.reflective-subuniverses

Idea

A reflective subuniverse is Σ-closed, or dependent-pair-closed, if its modal types are closed under the formation of dependent pair types.

Definition

Σ-closed modal operators

We say a modal operator ○ is Σ-closed if for every type X such that for every term of ○ X and for every type family P over X there is a section of ○ ∘ P, then there is also a term of ○ (Σ X P).

Note: this is not well-established terminology.

is-Σ-closed-operator-modality :
  {l1 l2 : Level} → operator-modality l1 l2 → UU (lsuc l1 ⊔ l2)
is-Σ-closed-operator-modality {l1} ○ =
  (X : UU l1) → ○ X → (P : X → UU l1) → ((x : X) → ○ (P x)) → ○ (Σ X P)

Σ-closed reflective subuniverses

is-Σ-closed-reflective-subuniverse :
  {l lM : Level} (U : reflective-subuniverse l lM) → UU (lsuc l ⊔ lM)
is-Σ-closed-reflective-subuniverse (○ , unit-○ , is-modal' , _) =
  is-Σ-closed-operator-modality (type-Prop ∘ is-modal')

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

See also

The equivalent notions of

• Higher modalities
• Uniquely eliminating modalities
• Stable orthogonal factorization systems

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)