∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
  (t :
    CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
      (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)),
  (CategoryTheory.Limits.Cocone.ofPushoutCocone t).ι =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagramIsoSpan F).hom t.ι