{-# OPTIONS --without-K --rewriting #-} open import lib.Basics open import lib.NType2 open import lib.types.Modality open import lib.types.Truncation module lib.modalities.Truncation where Trunc-modality : ∀ {i} n → Modality i Trunc-modality n = record { is-local = has-level n; is-local-is-prop = has-level-is-prop; ◯ = Trunc n; ◯-is-local = Trunc-level; η = [_]; ◯-elim = λ f → Trunc-elim {{λ {x} → f x}}; ◯-elim-β = λ _ _ _ → idp; ◯-=-is-local = λ _ _ → =-preserves-level Trunc-level}