Definition coproduct_PartialOrder : PartialOrder (setcoprod X Y). Proof. use make_PartialOrder. - exact coproduct_hrel. - exact isPartialOrder_coproduct_hrel. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.