Definition prod_directed_set {X Y : hSet} {PX : PartialOrder X} {PY : PartialOrder Y} (D₁ : directed_set PX) (D₂ : directed_set PY) : directed_set (prod_PartialOrder PX PY). Proof. use make_directed_set. - exact (D₁ × D₂). - exact (λ xy, D₁ (pr1 xy) ,, D₂ (pr2 xy)). - exact (is_directed_prod D₁ D₂). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.