Home

命題上の同一視型は可縮な型である

module foundations.prop-id-contr where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.proposition
open import foundations.contractible-type
open import foundations.sigma-type
open import foundations.greater-h-levels

private variable
  ℓ : Level
  A : Type ℓ
  x y : A

isProp⇒isContrId : isProp A → isContr (Id A x y)
isProp⇒isContrId {x = x} {y} f =
  f x y , isProp⇒isSet f x y (f x y)