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