Σ-closed modalities

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-06-28.
Last modified on 2024-11-19.

module orthogonal-factorization-systems.sigma-closed-modalities where
Imports 
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.sigma-closed-subuniverses
open import foundation.universe-levels

open import orthogonal-factorization-systems.modal-operators

Idea

A modal operator with unit is Σ-closed if its subuniverse of modal types is Σ-closed. I.e., if Σ A B is modal whenever B is a family of modal types over modal base A.

Definition

is-closed-under-Σ-modality :
  {l : Level} {○ : operator-modality l l} → unit-modality ○ → UU (lsuc l)
is-closed-under-Σ-modality =
  is-closed-under-Σ-subuniverse ∘ modal-type-subuniverse

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

See also

Recent changes