∀ {A : Type u_7} {B : Type u_8} {C : Type u_9} {A' : Type u_10} {B' : Type u_11} {C' : Type u_12}
  [inst : CategoryTheory.Category.{u_1, u_7} A] [inst_1 : CategoryTheory.Category.{u_2, u_8} B]
  [inst_2 : CategoryTheory.Category.{u_3, u_9} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{u_4, u_10} A'] [inst_4 : CategoryTheory.Category.{u_5, u_11} B']
  [inst_5 : CategoryTheory.Category.{u_6, u_12} C'] {F' : CategoryTheory.Functor A' B'}
  {G' : CategoryTheory.Functor C' B'} {W X Y Z : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (f : CategoryTheory.Limits.CatCospanTransformMorphism W X) (g : CategoryTheory.Limits.CatCospanTransformMorphism X Y)
  (h : CategoryTheory.Limits.CatCospanTransformMorphism Y Z),
  {
      left :=
        CategoryTheory.CategoryStruct.comp
          { left := CategoryTheory.CategoryStruct.comp f.left g.left,
              right := CategoryTheory.CategoryStruct.comp f.right g.right,
              base := CategoryTheory.CategoryStruct.comp f.base g.base, left_coherence := ⋯, right_coherence := ⋯ }.left
          h.left,
      right :=
        CategoryTheory.CategoryStruct.comp
          { left := CategoryTheory.CategoryStruct.comp f.left g.left,
              right := CategoryTheory.CategoryStruct.comp f.right g.right,
              base := CategoryTheory.CategoryStruct.comp f.base g.base, left_coherence := ⋯,
              right_coherence := ⋯ }.right
          h.right,
      base :=
        CategoryTheory.CategoryStruct.comp
          { left := CategoryTheory.CategoryStruct.comp f.left g.left,
              right := CategoryTheory.CategoryStruct.comp f.right g.right,
              base := CategoryTheory.CategoryStruct.comp f.base g.base, left_coherence := ⋯, right_coherence := ⋯ }.base
          h.base,
      left_coherence := ⋯, right_coherence := ⋯ } =
    {
      left :=
        CategoryTheory.CategoryStruct.comp f.left
          { left := CategoryTheory.CategoryStruct.comp g.left h.left,
              right := CategoryTheory.CategoryStruct.comp g.right h.right,
              base := CategoryTheory.CategoryStruct.comp g.base h.base, left_coherence := ⋯,
              right_coherence := ⋯ }.left,
      right :=
        CategoryTheory.CategoryStruct.comp f.right
          { left := CategoryTheory.CategoryStruct.comp g.left h.left,
              right := CategoryTheory.CategoryStruct.comp g.right h.right,
              base := CategoryTheory.CategoryStruct.comp g.base h.base, left_coherence := ⋯,
              right_coherence := ⋯ }.right,
      base :=
        CategoryTheory.CategoryStruct.comp f.base
          { left := CategoryTheory.CategoryStruct.comp g.left h.left,
              right := CategoryTheory.CategoryStruct.comp g.right h.right,
              base := CategoryTheory.CategoryStruct.comp g.base h.base, left_coherence := ⋯,
              right_coherence := ⋯ }.base,
      left_coherence := ⋯, right_coherence := ⋯ }