Proposition is_algebraic_is_directed {X : dcpo} (CX : is_algebraic_dcpo X) (x : X) : is_directed X (λ (z : ∑ (b : X), is_compact_el b ∧ b ≪ x), pr1 z). Proof. revert CX. use factor_through_squash_hProp. intros CX. pose (D := compact_approximating_family CX x). split. - assert (H := directed_set_el D). revert H. use factor_through_squash_hProp. intros d. use hinhpr. refine (D d ,, _). split. + apply is_compact_approximating_family. + apply compact_approximating_family_way_below. - intros [ b₁ p₁ ] [ b₂ p₂ ]. assert (x ⊑ ⨆ D) as q. { rewrite <- (compact_approximating_family_lub CX x). apply refl_dcpo. } assert (H := way_below_elem (pr2 p₁) D q). revert H. use factor_through_squash_hProp. intros [ c₁ r₁ ]. assert (H := way_below_elem (pr2 p₂) D q). revert H. use factor_through_squash_hProp. intros [ c₂ r₂ ]. assert (H := directed_set_top D c₁ c₂). revert H. use factor_through_squash_hProp. intros [ k [ s₂ s₃ ]]. use hinhpr. simple refine ((D k ,, _) ,, _ ,, _). + split. * apply is_compact_approximating_family. * apply compact_approximating_family_way_below. + exact (trans_dcpo r₁ s₂). + exact (trans_dcpo r₂ s₃). 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. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.