{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {X Y S X' Y' S' : C} →
        (f : X ⟶ S) →
          (g : Y ⟶ S) →
            (f' : X' ⟶ S') →
              (g' : Y' ⟶ S') →
                (i₁ : X ⟶ X') →
                  (i₂ : Y ⟶ Y') →
                    (i₃ : S ⟶ S') →
                      CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f' →
                        CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g' →
                          [CategoryTheory.Mono i₃] →
                            CategoryTheory.Limits.pullback
                                (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁)
                                (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂) ≅
                              CategoryTheory.Limits.pullback f g