{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          {t : CategoryTheory.Limits.PushoutCocone f g} →
            CategoryTheory.Limits.IsColimit t →
              {W : C} →
                (h : Y ⟶ W) →
                  (k : Z ⟶ W) →
                    CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k →
                      { l //
                        CategoryTheory.CategoryStruct.comp t.inl l = h ∧
                          CategoryTheory.CategoryStruct.comp t.inr l = k }