∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {D : Type u'} {inst_1 : CategoryTheory.Category.{v', u'} D}
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {x y : F.HomObj G A}, x = y ↔ x.app = y.app