Modal operators

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

Created on 2023-03-09.
Last modified on 2024-03-12.

module orthogonal-factorization-systems.modal-operators where
Imports 
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

Idea

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

Definitions

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 ○)
  where

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

  is-modal-family : {l3 : Level} {X : UU l3} (P : X → UU l1) → UU (l1 ⊔ l2 ⊔ l3)
  is-modal-family {X = X} P = (x : X) → is-modal (P x)

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

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

  is-property-is-modal : (X : UU l1) → is-prop (is-modal X)
  is-property-is-modal X = is-prop-type-Prop (is-modal-Prop 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)
  where

  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 =
    is-equiv-comp
      ( 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)
  where

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

References

[RSS20]
Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, 01 2020. URL: https://lmcs.episciences.org/6015, arXiv:1706.07526, doi:10.23638/LMCS-16(1:2)2020.

Recent changes