Modal operators

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2023-03-09.
Last modified on 2023-09-15.

module orthogonal-factorization-systems.modal-operators where
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.propositions
open import foundation.small-types
open import foundation.subuniverses
open import foundation.universe-levels


Underlying every modality is a modal operator, which is an operation on types that construct new types. For a monadic modality , there is moreover a modal unit that compares every type X to its modal type ○ X (X → ○ X).


operator-modality : (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
operator-modality l1 l2 = UU l1  UU l2
unit-modality : {l1 l2 : Level}  operator-modality l1 l2  UU (lsuc l1  l2)
unit-modality {l1}  = {X : UU l1}  X   X

The subuniverse of modal types

module _
  {l1 l2 : Level} { : operator-modality l1 l2} (unit-○ : unit-modality )

  is-modal : (X : UU l1)  UU (l1  l2)
  is-modal X = is-equiv (unit-○ {X})

  modal-type : UU (lsuc l1  l2)
  modal-type = Σ (UU l1) (is-modal)

  is-property-is-modal : (X : UU l1)  is-prop (is-modal X)
  is-property-is-modal X = is-property-is-equiv (unit-○ {X})

  is-modal-Prop : (X : UU l1)  Prop (l1  l2)
  pr1 (is-modal-Prop X) = is-modal X
  pr2 (is-modal-Prop X) = is-property-is-modal X

  is-subuniverse-is-modal : is-subuniverse is-modal
  is-subuniverse-is-modal = is-property-is-modal

  modal-type-subuniverse : subuniverse l1 (l1  l2)
  modal-type-subuniverse = is-modal-Prop

A small type is said to be modal if its small equivalent is modal.

is-modal-type-is-small :
  {l1 l2 l3 : Level}
  { : operator-modality l1 l2} (unit-○ : unit-modality )
  (X : UU l3) (is-small-X : is-small l1 X)  UU (l1  l2)
is-modal-type-is-small unit-○ X is-small-X =
  is-modal unit-○ (type-is-small is-small-X)

module _
  {l1 l2 l3 : Level}
  { : operator-modality l1 l2} (unit-○ : unit-modality )
  (X : UU l3) (is-small-X : is-small l1 X)

  is-equiv-unit-is-modal-type-is-small :
    is-modal-type-is-small unit-○ X is-small-X 
    is-equiv (unit-○  map-equiv-is-small is-small-X)
  is-equiv-unit-is-modal-type-is-small =
      ( unit-○)
      ( map-equiv-is-small is-small-X)
      ( is-equiv-map-equiv (equiv-is-small is-small-X))

  equiv-unit-is-modal-type-is-small :
    is-modal-type-is-small unit-○ X is-small-X 
    X   (type-is-small is-small-X)
  pr1 (equiv-unit-is-modal-type-is-small m) =
    unit-○  map-equiv-is-small is-small-X
  pr2 (equiv-unit-is-modal-type-is-small m) =
    is-equiv-unit-is-modal-type-is-small m

  map-inv-unit-is-modal-type-is-small :
    is-modal-type-is-small unit-○ X is-small-X 
     (type-is-small is-small-X)  X
  map-inv-unit-is-modal-type-is-small =
    map-inv-equiv  equiv-unit-is-modal-type-is-small

module _
  {l1 l2 : Level} (l3 : Level)
  { : operator-modality l1 l2} (unit-○ : unit-modality )
  (X : Small-Type l1 l3)

  is-modal-Small-Type : UU (l1  l2)
  is-modal-Small-Type =
    is-modal-type-is-small unit-○
      ( type-Small-Type X)
      ( is-small-type-Small-Type X)

  is-equiv-unit-is-modal-Small-Type :
    is-equiv (unit-○  map-equiv (equiv-is-small-type-Small-Type X))
  is-equiv-unit-is-modal-Small-Type =
    is-equiv-unit-is-modal-type-is-small unit-○
      ( type-Small-Type X)
      ( is-small-type-Small-Type X)

  equiv-unit-is-modal-Small-Type :
    is-modal-Small-Type  type-Small-Type X   (small-type-Small-Type X)
  equiv-unit-is-modal-Small-Type =
    equiv-unit-is-modal-type-is-small unit-○
      ( type-Small-Type X)
      ( is-small-type-Small-Type X)

  map-inv-unit-is-modal-Small-Type :
    is-modal-Small-Type   (small-type-Small-Type X)  type-Small-Type X
  map-inv-unit-is-modal-Small-Type =
    map-inv-equiv  equiv-unit-is-modal-Small-Type


  • 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)

Recent changes