Definition is_monotone_set_coproduct_map {Z : hSet} {PZ : PartialOrder Z} {f : ∏ (x : X), Y x → Z} (Pf : ∏ (x : X), is_monotone (PY x) PZ (f x)) : is_monotone coproduct_set_PartialOrder PZ (λ xy, f (pr1 xy) (pr2 xy)).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.