Categories where coproduct injections are mono

Stream: maths

[Joël Riou]

In the development of split simplicial objects (see #16274, which will be followed by some examples and a study of their skeleta), I need to introduce a class for categories where inclusions like A ⟶ A ⨿ Bare monomorphisms. Would you think mono_coprod_in be a suitable name?

variables (C : Type*) [category C] [has_finite_coproducts C]
class mono_coprod_in : Prop :=
(mono_coprod_inl' : Π (A B : C), mono (coprod.inl : A ⟶ A ⨿ B))

(This is true for the category of sets, and categories that have zero morphisms.)

[Scott Morrison]

@Joël Riou, did you introduce this? (I didn't see this earlier.) I think I would like this definition for something else, too. Perhaps just mono_coprod suffices as a name, as it's not entirely clear what the _in is referring to.

[Joël Riou]

Ok for mono_coprod. I have not yet PRed this. I could do it soon, once PR #16444 is merged.