module foundations.contractible-type where
open import foundations.universe open import foundations.sigma-type open import foundations.identity-type
private variable ℓ : Level isContr : Type ℓ → Type ℓ isContr A = Σ[ x ∈ A ] ∀ (y : A) → x ＝ y
isContr Aの第一成分をcenterと呼ぶことがある。