Separating set in the category of ind-objects

We construct a separating set in the category of ind-objects.

Future work

Once we have constructed zero morphisms in the category of ind-objects, we will be able to show that under sufficient conditions, the category of ind-objects has a separating object.

theorem CategoryTheory.Ind.isSeparating_range_yoneda {C : Type u} [Category.{v, u} C] : IsSeparating (Set.range Ind.yoneda.obj)