Identity types of truncated types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Eléonore Mangel.

Created on 2022-05-16.
Last modified on 2023-06-08.

module foundation.identity-truncated-types where
Imports 
open import foundation.univalence
open import foundation.universe-levels

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

The type of identity of truncated types is truncated

module _
  {l : Level} {A B : UU l}
  where

  is-trunc-id-is-trunc :
    (k : 𝕋) → is-trunc k A → is-trunc k B → is-trunc k (A ＝ B)
  is-trunc-id-is-trunc k is-trunc-A is-trunc-B =
    is-trunc-equiv k
      ( A ≃ B)
      ( equiv-univalence)
      ( is-trunc-equiv-is-trunc k is-trunc-A is-trunc-B)

Recent changes