∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J],
  CategoryTheory.Mono (CategoryTheory.Limits.wideEqualizer.ι f)