∀ {A : Type u_12} {B : Type u_16} {C : Type u_13} [inst : CategoryTheory.Category.{u_10, u_12} A]
  [inst_1 : CategoryTheory.Category.{u_14, u_16} B] [inst_2 : CategoryTheory.Category.{u_11, u_13} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u_4} {B₁ : Type u_8} {C₁ : Type u_5}
  [inst_3 : CategoryTheory.Category.{u_2, u_4} A₁] [inst_4 : CategoryTheory.Category.{u_6, u_8} B₁]
  [inst_5 : CategoryTheory.Category.{u_3, u_5} C₁] {F₁ : CategoryTheory.Functor A₁ B₁}
  {G₁ : CategoryTheory.Functor C₁ B₁} {X : Type u_1} {Y : Type u_9} [inst_6 : CategoryTheory.Category.{u_7, u_1} X]
  [inst_7 : CategoryTheory.Category.{u_15, u_9} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (U : CategoryTheory.Functor X Y) {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y} (f : x ⟶ y),
  CategoryTheory.CategoryStruct.comp
      ((((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).comp
            ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).map
        f)
      ((fun x =>
            CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso (U.associator x.fst ψ.left)
              (U.associator x.snd ψ.right) ⋯)
          y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mkIso (U.associator x.fst ψ.left)
              (U.associator x.snd ψ.right) ⋯)
          x).hom
      ((((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ).comp
            ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).map
        f)