{J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            (t : CategoryTheory.Limits.Trident f) →
              ((s : CategoryTheory.Limits.Trident f) →
                  { l //
                    CategoryTheory.CategoryStruct.comp l t.ι = s.ι ∧
                      ∀
                        {m :
                          ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj s.pt).obj
                              CategoryTheory.Limits.WalkingParallelFamily.zero ⟶
                            ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj
                                  t.pt).obj
                              CategoryTheory.Limits.WalkingParallelFamily.zero},
                        CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = l }) →
                CategoryTheory.Limits.IsLimit t