∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D]
  (X : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D))
  (P : CategoryTheory.Idempotents.Karoubi C),
  (((CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso C D).inv.app X).app P).f = (X.map P.decompId_i).f