∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
  (z : F.obj CategoryTheory.Limits.WalkingCospan.one ≅ G.obj CategoryTheory.Limits.WalkingCospan.one)
  (l : F.obj CategoryTheory.Limits.WalkingCospan.left ≅ G.obj CategoryTheory.Limits.WalkingCospan.left)
  (r : F.obj CategoryTheory.Limits.WalkingCospan.right ≅ G.obj CategoryTheory.Limits.WalkingCospan.right),
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) z.hom =
      CategoryTheory.CategoryStruct.comp l.hom (G.map CategoryTheory.Limits.WalkingCospan.Hom.inl) →
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) z.hom =
        CategoryTheory.CategoryStruct.comp r.hom (G.map CategoryTheory.Limits.WalkingCospan.Hom.inr) →
      ∀ {X Y : CategoryTheory.Limits.WalkingCospan} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f)
            (Option.casesOn Y z fun val => CategoryTheory.Limits.WalkingPair.casesOn val l r).hom =
          CategoryTheory.CategoryStruct.comp
            (Option.casesOn X z fun val => CategoryTheory.Limits.WalkingPair.casesOn val l r).hom (G.map f)