Definition coproduct_hrel : hrel (setcoprod X Y). Proof. intros xy₁ xy₂. induction xy₁ as [ x₁ | y₁ ] ; induction xy₂ as [ x₂ | y₂ ]. - exact (PX x₁ x₂). - exact hfalse. - exact hfalse. - exact (PY y₁ y₂). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.