This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Σ-closed reflective modalities

module orthogonal-factorization-systems.sigma-closed-reflective-modalities where
Imports 
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import orthogonal-factorization-systems.modal-operators
open import orthogonal-factorization-systems.reflective-modalities
open import orthogonal-factorization-systems.sigma-closed-modalities

Idea

A modality is Σ-closed reflective if it is reflective and Σ-closed.

Definition

is-closed-under-Σ-reflective-modality :
  {l : Level} {○ : operator-modality l l} →
  (unit-○ : unit-modality ○) → UU (lsuc l)
is-closed-under-Σ-reflective-modality unit-○ =
  (is-reflective-modality unit-○) × (is-closed-under-Σ-modality unit-○)

closed-under-Σ-reflective-modality : (l : Level) → UU (lsuc l)
closed-under-Σ-reflective-modality l =
  Σ ( operator-modality l l)
    ( λ ○ →
      Σ ( unit-modality ○)
        ( is-closed-under-Σ-reflective-modality))

See also

The equivalent notions of