∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (F : CategoryTheory.Functor C (Type u_3)) {X : C}
  (x : F.obj X) {X_1 Y : CategoryTheory.Over (F.elementsMk X x)} (f : X_1 ⟶ Y),
  ↑(CategoryTheory.CategoryStruct.comp f.left Y.hom) = ↑X_1.hom