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

Reflective modalities

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

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

Idea

A modal operator with unit is reflective if its subuniverse of modal types is reflective.

Definitions

Reflective subuniverses

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

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

See also