∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {T : Type u_3}
  (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)) (t : T) [inst_1 : Subsingleton T] (X : C),
  CategoryTheory.StructuredArrow.homMk (CategoryTheory.CategoryStruct.id X) ⋯ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.StructuredArrow.mk (CategoryTheory.eqToHom ⋯))