∀ {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] (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X),
  {
      app := fun x =>
        { fst := (CategoryTheory.CategoryStruct.id X_1).fst.app x,
          snd := (CategoryTheory.CategoryStruct.id X_1).snd.app x, w := ⋯ },
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id
      { obj := fun x => { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x },
        map := fun {x y} f => { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }