∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  (X : CategoryTheory.InducedCategory D F),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id (F X)