∀ (V : Type u_3) [inst : CategoryTheory.Category.{u_2, u_3} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{u_4, u_1} D] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D]
  (x : Dᵒᵖ),
  CategoryTheory.EnrichedOrdinaryCategory.homEquiv (CategoryTheory.CategoryStruct.id (Opposite.unop x)) =
    CategoryTheory.eId V (Opposite.unop x)