Definition set_coproduct_hrel : hrel (∑ (x : X), Y x)%set := λ xy₁ xy₂, let x₁ := pr1 xy₁ in let x₂ := pr1 xy₂ in let y₁ := pr2 xy₁ in let y₂ := pr2 xy₂ in (∑ (p : eqset x₁ x₂), PY x₂ (transportf Y p y₁) y₂)%prop.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.