Proposition is_directed_prod {X Y : hSet} {PX : PartialOrder X} {PY : PartialOrder Y} (D₁ : directed_set PX) (D₂ : directed_set PY) : is_directed (prod_PartialOrder PX PY) (λ (xy : D₁ × D₂), D₁ (pr1 xy),, D₂ (pr2 xy)). Proof. split. - assert (i₁ := directed_set_el D₁). assert (i₂ := directed_set_el D₂). apply hinhand; assumption. - intros ij₁ ij₂. induction ij₁ as [ i₁ j₁ ]. induction ij₂ as [ i₂ j₂ ]. assert (k₁ := directed_set_top D₁ i₁ i₂). assert (k₂ := directed_set_top D₂ j₁ j₂). simple refine (hinhuniv2 _ k₁ k₂). clear k₁ k₂. intros k₁ k₂. induction k₁ as [ k₁ [ H₁ H₂ ]]. induction k₂ as [ k₂ [ H₃ H₄ ]]. refine (hinhpr ((k₁ ,, k₂) ,, _)) ; cbn. split. + exact (H₁ ,, H₃). + exact (H₂ ,, H₄). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions.