∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  (e : F.CorepresentableBy X) {Y : C} (f : X ⟶ Y),
  e.homEquiv f = F.map f (e.homEquiv (CategoryTheory.CategoryStruct.id X))