{P : Sort u} →
  {C : Type u_1} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {P_1 Q : CategoryTheory.Idempotents.Karoubi C} →
        {t : P_1.Hom Q} →
          {C' : Type u_1} →
            {inst' : CategoryTheory.Category.{v_1, u_1} C'} →
              {P' Q' : CategoryTheory.Idempotents.Karoubi C'} →
                {t' : P'.Hom Q'} →
                  C = C' →
                    inst ≍ inst' →
                      P_1 ≍ P' → Q ≍ Q' → t ≍ t' → CategoryTheory.Idempotents.Karoubi.Hom.noConfusionType P t t'