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 _ _