∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)}
  (e₁ e₁_1 :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G))
  (e_e₁ : e₁ = e₁_1)
  (e₂ e₂_1 :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G))
  (e_e₂ : e₂ = e₂_1)
  (coh :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom F)
        (CategoryTheory.CategoryStruct.comp (K.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
          (CategoryTheory.CategoryStruct.comp
            (K.whiskerLeft
              (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                  (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
            (K.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv)) =
      CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
        (CategoryTheory.CategoryStruct.comp
          (J.whiskerLeft
            (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
          (CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv
            (CategoryTheory.Functor.whiskerRight e₂.hom G)))),
  CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁ e₂ coh =
    CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁_1 e₂_1 ⋯