∀ {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 A' : (CategoryTheory.Functor C (Type w))ᵒᵖ} (f : A ⟶ A')
  (x : F.HomObj G (Opposite.unop A)) (X : C) (a : (Opposite.unop A').obj X),
  ((F.homObjFunctor G).map f x).app X a = x.app X (f.unop.app X a)