∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} 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.Cocone (CategoryTheory.Limits.parallelFamily f))
      (j : CategoryTheory.Limits.WalkingParallelFamily J),
      CategoryTheory.CategoryStruct.comp (t.ι.app j) (desc s) = s.ι.app j