∀ {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]
  {s t : CategoryTheory.Limits.Trident f} (k : s.pt ⟶ t.pt),
  CategoryTheory.CategoryStruct.comp k t.ι = s.ι →
    ∀ (j : CategoryTheory.Limits.WalkingParallelFamily J), CategoryTheory.CategoryStruct.comp k (t.π.app j) = s.π.app j