Proposition isPartialOrder_set_coproduct_hrel : isPartialOrder set_coproduct_hrel. Proof. repeat split. - intros xy₁ xy₂ xy₃ pq₁ pq₂. induction xy₁ as [ x₁ y₁ ]. induction xy₂ as [ x₂ y₂ ]. induction xy₃ as [ x₃ y₃ ]. induction pq₁ as [ p₁ q₁ ]. induction pq₂ as [ p₂ q₂ ]. cbn in *. induction p₁, p₂ ; cbn in *. refine (idpath _ ,, _) ; cbn. exact (trans_PartialOrder (PY _) q₁ q₂). - intros xy. induction xy as [ x y ] ; cbn. refine (idpath _ ,, _). exact (refl_PartialOrder (PY x) y). - intros xy₁ xy₂ pq₁ pq₂. induction xy₁ as [ x₁ y₁ ]. induction xy₂ as [ x₂ y₂ ]. induction pq₁ as [ p₁ q₁ ]. induction pq₂ as [ p₂ q₂ ]. cbn in *. induction p₁ ; cbn in *. assert (p₂ = idpath _) as r. { apply setproperty. } rewrite r in q₂ ; clear p₂ r. cbn in q₂. apply maponpaths. exact (antisymm_PartialOrder (PY _) q₁ q₂). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.