Proposition prod_PartialOrderLaws : isPartialOrder R. Proof. simple refine ((_ ,, _) ,, _). - refine (λ x y z p q, _ ,, _). + exact (trans_PartialOrder R₁ (pr1 p) (pr1 q)). + exact (trans_PartialOrder R₂ (pr2 p) (pr2 q)). - refine (λ x, _ ,, _). + exact (refl_PartialOrder R₁ (pr1 x)). + exact (refl_PartialOrder R₂ (pr2 x)). - refine (λ x y p q, _). use pathsdirprod. + exact (antisymm_PartialOrder R₁ (pr1 p) (pr1 q)). + exact (antisymm_PartialOrder R₂ (pr2 p) (pr2 q)). Qed.
Require Import UniMath.MoreFoundations.All.