fact: Definition is_monotone_sumofmaps {Z : hSet} {PZ : PartialOrder Z} {f : X → Z} (Pf : is_monotone PX PZ f) {g : Y → Z} (Pg : is_monotone PY PZ g) : is_monotone coproduct_PartialOrder PZ (sumofmaps f g).
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions