Proposition is_continuous_dcpo_is_directed {X : dcpo} (CX : is_continuous_dcpo X) (x : X) : is_directed X (λ (z : ∑ (b : X), b ≪ x), pr1 z). Proof. revert CX. use factor_through_squash_hProp. intros CX. pose (D := 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 ,, _). apply approximating_family_way_below. - intros [ b₁ p₁ ] [ b₂ p₂ ]. assert (x ⊑ ⨆ D) as q. { rewrite <- (approximating_family_lub CX x). apply refl_dcpo. } assert (H := way_below_elem p₁ D q). revert H. use factor_through_squash_hProp. intros [ c₁ r₁ ]. assert (H := way_below_elem 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 ,, _) ,, _ ,, _). + apply 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.