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