∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} [inst_2 : F.Full] [F.Faithful] {c : C} {a_1 b_1 : c ⟶ hf'.pullback g},
  CategoryTheory.CategoryStruct.comp a_1 (hf'.fst' g) = CategoryTheory.CategoryStruct.comp b_1 (hf'.fst' g) →
    CategoryTheory.CategoryStruct.comp a_1 (hf'.snd g) = CategoryTheory.CategoryStruct.comp b_1 (hf'.snd g) → a_1 = b_1