∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : P ⟶ Q},
  (∀ (X : C) (p : CategoryTheory.yoneda.obj X ⟶ P),
      CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g) →
    f = g