{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          [inst_2 : F.Full] →
            {A₁ A₂ A₃ : C} →
              {X : D} →
                {f₁ : F.obj A₁ ⟶ X} →
                  (hf₁ : F.relativelyRepresentable f₁) →
                    (f₂ : F.obj A₂ ⟶ X) →
                      (f₃ : F.obj A₃ ⟶ X) →
                        [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] →
                          [F.Faithful] →
                            {Z : C} →
                              (x₁ : Z ⟶ A₁) →
                                (x₂ : Z ⟶ A₂) →
                                  (x₃ : Z ⟶ A₃) →
                                    CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ =
                                        CategoryTheory.CategoryStruct.comp (F.map x₂) f₂ →
                                      CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ =
                                          CategoryTheory.CategoryStruct.comp (F.map x₃) f₃ →
                                        (Z ⟶ hf₁.pullback₃ f₂ f₃)