Definition coproduct_set_PartialOrder : PartialOrder (∑ (x : X), Y x)%set. Proof. use make_PartialOrder. - exact set_coproduct_hrel. - exact isPartialOrder_set_coproduct_hrel. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.