∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} D] (F : C → D)
  {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y),
  CategoryTheory.InducedCategory.homMk ((CategoryTheory.inducedFunctor F).map f) = f