Home

冪等射

open import category-theory.category

module category-theory.idempotent-morphism {o h} (𝒞 : Category o h) where
Imports 
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 _ _