no goals
C : Type ?u.50202
inst✝ : Category C
P Q : Karoubi C
f : P ⟶ Q
⊢ mk P.X (𝟙 P.X) ⟶ mk Q.X (𝟙 Q.X)
exact Hom.mk f.f (by simp)
no goals
C : Type ?u.50202
inst✝ : Category C
P Q : Karoubi C
f : P ⟶ Q
⊢ f.f = (mk P.X (𝟙 P.X)).p ≫ f.f ≫ (mk Q.X (𝟙 Q.X)).p
simp
no goals
C : Type u_1
inst✝ : Category C
P Q : Karoubi C
f : P ⟶ Q
⊢ f ≫ decompId_i Q = decompId_i P ≫ Hom.mk f.f
aesop_cat