Stability properties of monomorphisms in Type

In this file, we show that in the category Type u, monomorphisms are stable under cobase change, filtered colimits. After importing Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean, the fact that monomorphisms are stable under transfinite composition will also be inferred automatically.

(The stability by retracts holds in any category: it is shown in the file Mathlib/CategoryTheory/MorphismProperty/Retract.lean.)

instance CategoryTheory.Types.instIsStableUnderCobaseChangeMonomorphismsType : (MorphismProperty.monomorphisms (Type u)).IsStableUnderCobaseChange

instance CategoryTheory.Types.instIsStableUnderFilteredColimitsMonomorphismsType : MorphismProperty.IsStableUnderFilteredColimits.{v', u', u, u + 1} (MorphismProperty.monomorphisms (Type u))

instance CategoryTheory.Types.instIsStableUnderCoproductsOfShapeMonomorphismsType (T : Type u') : (MorphismProperty.monomorphisms (Type u)).IsStableUnderCoproductsOfShape T

instance CategoryTheory.Types.instIsStableUnderCoproductsMonomorphismsType : MorphismProperty.IsStableUnderCoproducts.{u_1, u, u + 1} (MorphismProperty.monomorphisms (Type u))