English
If forgetful functor forget C preserves colimits of shape Discrete WalkingPair and reflects monomorphisms, then MonoCoprod C holds.
Русский
Если забывающий функтор forget C сохраняет колимиты формы Discrete WalkingPair и отражает моно-морфизмы, то MonoCoprod C существует.
LaTeX
$$$[Forget\\ C]\\;\\text{ preservesColimitsOfShape }(Discrete\\ WalkingPair)\\ F\\lor [Forget\\ C].ReflectsMonomorphisms \\Rightarrow MonoCoprod\\ C$$$
Lean4
instance [HasForget C] [PreservesColimitsOfShape (Discrete WalkingPair) (forget C)] [ReflectsMonomorphisms (forget C)] :
MonoCoprod C :=
monoCoprod_of_preservesCoprod_of_reflectsMono (forget C)
