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).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.