Proposition is_directed_unary_interpolation_directed_set : is_directed X (λ (ij : ∑ (i : D), D_a i), D_a (pr1 ij) (pr2 ij)). Proof. split. - assert (H := directed_set_el D). revert H. use factor_through_squash ; [ apply propproperty | ]. intro i. assert (H := directed_set_el (D_a i)). revert H. use factor_through_squash ; [ apply propproperty | ]. intro j. exact (hinhpr (i ,, j)). - intros ij₁ ij₂. induction ij₁ as [ i₁ j₁ ]. induction ij₂ as [ i₂ j₂ ]. assert (H := directed_set_top D i₁ i₂). revert H. use factor_through_squash ; [ apply propproperty | ]. intros k. induction k as [ k [ q₁ q₂ ]]. assert (H := unary_interpolation_cofinal q₁ j₁). revert H. use factor_through_squash ; [ apply propproperty | ]. intros H₁. induction H₁ as [ l₁ H₁ ]. assert (H := unary_interpolation_cofinal q₂ j₂). revert H. use factor_through_squash ; [ apply propproperty | ]. intros H₂. induction H₂ as [ l₂ H₂ ]. assert (H := directed_set_top (D_a k) l₁ l₂). revert H. use factor_through_squash ; [ apply propproperty | ]. intros H. induction H as [ m [ r₁ r₂ ]]. refine (hinhpr ((k ,, m) ,, _ ,, _)). + exact (trans_dcpo H₁ r₁). + exact (trans_dcpo H₂ r₂). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.