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