∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {W : C}
  {φ₁ φ₂ : W ⟶ CategoryTheory.ChosenPullbacksAlong.pullbackObj f g},
  φ₁ = φ₂ ↔
    CategoryTheory.CategoryStruct.comp φ₁ (CategoryTheory.ChosenPullbacksAlong.fst f g) =
        CategoryTheory.CategoryStruct.comp φ₂ (CategoryTheory.ChosenPullbacksAlong.fst f g) ∧
      CategoryTheory.CategoryStruct.comp φ₁ (CategoryTheory.ChosenPullbacksAlong.snd f g) =
        CategoryTheory.CategoryStruct.comp φ₂ (CategoryTheory.ChosenPullbacksAlong.snd f g)