open import category-theory.category module category-theory.idempotent-morphism {o h} (𝒞 : Category o h) where
open import foundations.universe open import foundations.identity-type open import foundations.proposition open Category 𝒞
private variable A : Ob isIdempotent : Hom A A → Type h isIdempotent f = f ∘ f = f
冪等射であるということは命題である。
private variable f : Hom A A isPropIsIdempotent : isProp (isIdempotent f) isPropIsIdempotent = is-set-hom _ _