∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {A' : Type u_7} {B' : Type u_8} {C' : Type u_9}
  [inst : CategoryTheory.Category.{u_10, u_1} A] [inst_1 : CategoryTheory.Category.{u_11, u_2} B]
  [inst_2 : CategoryTheory.Category.{u_12, u_3} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{u_4, u_7} A'] [inst_4 : CategoryTheory.Category.{u_5, u_8} B']
  [inst_5 : CategoryTheory.Category.{u_6, u_9} C'] {F' : CategoryTheory.Functor A' B'}
  {G' : CategoryTheory.Functor C' B'} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right) (base : ψ.base ≅ ψ'.base)
  (left_coherence :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
        (CategoryTheory.Functor.whiskerRight left.hom F') =
      CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom)
        (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
  (right_coherence :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
        (CategoryTheory.Functor.whiskerRight right.hom G') =
      CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom)
        (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom),
  CategoryTheory.CategoryStruct.comp
      { left := left.hom, right := right.hom, base := base.hom, left_coherence := ⋯, right_coherence := ⋯ }
      { left := left.inv, right := right.inv, base := base.inv, left_coherence := ⋯, right_coherence := ⋯ } =
    CategoryTheory.CategoryStruct.id ψ