Proposition isPartialOrder_coproduct_hrel : isPartialOrder coproduct_hrel. Proof. repeat split. - intros xy₁ xy₂ xy₃ p q. induction xy₁ as [ x₁ | y₁ ] ; induction xy₂ as [ x₂ | y₂ ] ; induction xy₃ as [ x₃ | y₃ ] ; cbn ; cbn in p, q ; try (apply (fromempty p)) ; try (apply (fromempty q)). + exact (trans_PartialOrder PX p q). + exact (trans_PartialOrder PY p q). - intros xy ; induction xy as [ x | y ] ; cbn. + exact (refl_PartialOrder PX x). + exact (refl_PartialOrder PY y). - intros xy₁ xy₂ p q. induction xy₁ as [ x₁ | y₁ ] ; induction xy₂ as [ x₂ | y₂ ] ; cbn in p, q ; try (apply (fromempty p)) ; try (apply (fromempty q)). + exact (maponpaths inl (antisymm_PartialOrder PX p q)). + exact (maponpaths inr (antisymm_PartialOrder PY p q)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.