∀ {C : Type u_1} {D : Type u_4} [inst : CategoryTheory.Category.{u_2, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D]
  {F G : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D} (τ : F ⟶ G),
  {
      app := fun P =>
        CategoryTheory.CategoryStruct.comp (F.map P.decompId_i)
          (CategoryTheory.CategoryStruct.comp
            ((((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) D).obj
                      (CategoryTheory.Idempotents.toKaroubi C)).map
                  τ).app
              P.X)
            (G.map P.decompId_p)),
      naturality := ⋯ } =
    τ