∀ {A : Type u_5} {B : Type u_6} {C : Type u_7} [inst : CategoryTheory.Category.{u_1, u_5} A]
  [inst_1 : CategoryTheory.Category.{u_2, u_6} B] [inst_2 : CategoryTheory.Category.{u_3, u_7} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u_8)
  [inst_3 : CategoryTheory.Category.{u_4, u_8} X]
  {W X_1 Y Z : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (f : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X W X_1)
  (g : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X X_1 Y)
  (h : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X Y Z),
  {
      fst :=
        CategoryTheory.CategoryStruct.comp
          { fst := CategoryTheory.CategoryStruct.comp f.fst g.fst,
              snd := CategoryTheory.CategoryStruct.comp f.snd g.snd, w := ⋯ }.fst
          h.fst,
      snd :=
        CategoryTheory.CategoryStruct.comp
          { fst := CategoryTheory.CategoryStruct.comp f.fst g.fst,
              snd := CategoryTheory.CategoryStruct.comp f.snd g.snd, w := ⋯ }.snd
          h.snd,
      w := ⋯ } =
    {
      fst :=
        CategoryTheory.CategoryStruct.comp f.fst
          { fst := CategoryTheory.CategoryStruct.comp g.fst h.fst,
              snd := CategoryTheory.CategoryStruct.comp g.snd h.snd, w := ⋯ }.fst,
      snd :=
        CategoryTheory.CategoryStruct.comp f.snd
          { fst := CategoryTheory.CategoryStruct.comp g.fst h.fst,
              snd := CategoryTheory.CategoryStruct.comp g.snd h.snd, w := ⋯ }.snd,
      w := ⋯ }