{J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            (t : CategoryTheory.Limits.Cotrident f) →
              (desc : (s : CategoryTheory.Limits.Cotrident f) → t.pt ⟶ s.pt) →
                (∀ (s : CategoryTheory.Limits.Cotrident f), CategoryTheory.CategoryStruct.comp t.π (desc s) = s.π) →
                  (∀ (s : CategoryTheory.Limits.Cotrident f) (m : t.pt ⟶ s.pt),
                      (∀ (j : CategoryTheory.Limits.WalkingParallelFamily J),
                          CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) →
                        m = desc s) →
                    CategoryTheory.Limits.IsColimit t