no goals
C : Type ?u.15232
inst✝ : Category C
P : Karoubi C
⊢ P.p = P.p ≫ P.p ≫ P.p
repeat' rw [P.idem]
no goals
C : Type ?u.15232
inst✝ : Category C
P : Karoubi C
⊢ P.p = P.p ≫ P.p
rw [P.idem]
no goals
C : Type u_1
inst✝ : Category C
P : Karoubi C
⊢ 𝟙 P = Hom.mk P.p
rfl