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