# The raise modalities

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-06-08.

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