∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {a : C} (x : F.obj a)
  (y : G.obj a), CategoryTheory.Limits.prod.fst.app a (CategoryTheory.FunctorToTypes.prodMk x y) = x