∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {F : CategoryTheory.Functor C (Type u_1)} {X : C}
  (h : F.CorepresentableBy X) (Y : F.Elements),
  F.map (h.homEquiv.symm Y.snd) (CategoryTheory.Functor.Elements.initialOfCorepresentableBy h).snd = Y.snd