This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Truncated equality

module foundation.truncated-equality where

open import foundation.truncations
open import foundation.universe-levels

open import foundation-core.identity-types
open import foundation-core.truncated-types
open import foundation-core.truncation-levels

Definition

trunc-eq : {l : Level} (k : 𝕋) {A : UU l} → A → A → Truncated-Type l k
trunc-eq k x y = trunc k (x ＝ y)