Truncated equality

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-03-14.
Last modified on 2023-06-08.

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)

Recent changes

• 2023-06-08. Fredrik Bakke. Remove empty foundation modules and replace them by their core counterparts (#644).
• 2023-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).
• 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
• 2023-03-07. Fredrik Bakke. Add blank lines between <details> tags and markdown syntax (#490).
• 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).