Proposition is_algebraic_dcpo_directed_set_lub {X : dcpo} (CX : is_algebraic_dcpo X) (x : X) : ⨆ (is_algebraic_dcpo_directed_set CX x) = x. Proof. revert CX. use factor_dep_through_squash. { intro. apply setproperty. } intros CX. pose (D := compact_approximating_family CX x). cbn. use antisymm_dcpo. - use dcpo_lub_is_least. intros i. apply way_below_to_le. exact (pr22 i). - refine (trans_dcpo _ _). { apply eq_to_le_dcpo. exact (!(compact_approximating_family_lub CX x)). } use dcpo_lub_is_least. intros i. use less_than_dcpo_lub ; cbn -[way_below]. + refine (D i ,, _). split. * apply is_compact_approximating_family. * apply compact_approximating_family_way_below. + apply refl_dcpo. 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.