∀ {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],
  CategoryTheory.Idempotents.whiskeringLeftObjToKaroubiFullyFaithful =
    {
      preimage := fun {F G} τ =>
        {
          app := fun P =>
            CategoryTheory.CategoryStruct.comp (F.map P.decompId_i)
              (CategoryTheory.CategoryStruct.comp (τ.app P.X) (G.map P.decompId_p)),
          naturality := ⋯ },
      map_preimage := ⋯, preimage_map := ⋯ }