∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)} (f : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp P.p.f f.f.f = CategoryTheory.CategoryStruct.comp f.f.f Q.p.f