The raise modalities

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-06-08.
Last modified on 2023-11-24.

module orthogonal-factorization-systems.raise-modalities where
Imports 
open import foundation.function-types
open import foundation.raising-universe-levels
open import foundation.universe-levels

open import orthogonal-factorization-systems.local-types
open import orthogonal-factorization-systems.modal-operators
open import orthogonal-factorization-systems.uniquely-eliminating-modalities

Idea

The operations of raising universe levels are trivially higher modalities, and in the case that l1 ⊔ l2 = l1, we recover the identity modality.

Definition

operator-raise-modality :
  (l1 l2 : Level) → operator-modality l1 (l1 ⊔ l2)
operator-raise-modality l1 l2 = raise l2

unit-raise-modality :
  {l1 l2 : Level} → unit-modality (operator-raise-modality l1 l2)
unit-raise-modality = map-raise

Properties

The raise modality is a uniquely eliminating modality

is-uniquely-eliminating-modality-raise-modality :
  {l1 l2 : Level} →
  is-uniquely-eliminating-modality (unit-raise-modality {l1} {l2})
is-uniquely-eliminating-modality-raise-modality {l1} {l2} P =
  is-local-dependent-type-is-equiv
    ( unit-raise-modality)
    ( is-equiv-map-raise)
    ( operator-raise-modality l1 l2 ∘ P)

In the case that l1 ⊔ l2 = l1 we recover the identity modality

This remains to be made formal. #739

Recent changes