The truncation modalities

Content created by Fredrik Bakke and Egbert Rijke.

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

module foundation.truncation-modalities where
Imports 
open import foundation.truncations
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.truncation-levels

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

Idea

The truncation operations are higher modalities.

Definition

operator-trunc-modality :
  (l : Level) (k : 𝕋) → operator-modality l l
operator-trunc-modality _ = type-trunc

unit-trunc-modality :
  {l : Level} {k : 𝕋} → unit-modality (operator-trunc-modality l k)
unit-trunc-modality = unit-trunc

Properties

The truncation modalities are uniquely eliminating modalities

is-uniquely-eliminating-modality-trunc-modality :
  {l : Level} {k : 𝕋} →
  is-uniquely-eliminating-modality (unit-trunc-modality {l} {k})
is-uniquely-eliminating-modality-trunc-modality {k = k} P =
  dependent-universal-property-trunc (trunc k ∘ P)

Recent changes