MODAL SPACES

(Modality).

(Synonyms). The followin are equivalent: 1) Higher modalities; 2) -closed reflective subuniverses; 3) Stable orthogonal factorization systems.

(Modality System).

def Modality :=
  Σ (modality: U → U)
    (isModal : U → U)
    (eta:      Π (A : U), A → modality A)
    (elim:     Π (A : U) (B : modality A → U)
                 (B-Modal : Π (x : modality A), isModal (B x))
                 (f: П (x : A), (B (eta A x))),
                 (Π (x : modality A), B x))
    (elim-β :  Π (A : U) (B : modality A → U)
                 (B-Modal : Π (x : modality A), isModal (B x))
                 (f : Π (x : A), (B (eta A x))) (a : A),
                 PathP (<_>B (eta A a)) (elim A B B-Modal f (eta A a)) (f a))
    (modalityIsModal : Π (A : U), isModal (modality A))
    (propIsModal : Π (A : U), Π (a b : isModal A),
                     PathP (<_>isModal A) a b)
    (=-Modal : Π (A : U) (x y : modality A),
                 isModal (PathP (<_>modality A) x y)), 𝟏

LITERATURE

[1]. E.Rijke, M.Shulman, B.Spitters. Modalities in Homotopy Type Theory.