proposition: Proposition discrete_dcpo_lub {A : hSet} (D : directed_set (discrete_dcpo A)) (i : D) : ⨆ D = D i.
proof: Proof. use antisymm_dcpo. - use dcpo_lub_is_least. intro j. cbn. assert (H := directed_set_top D i j). revert H. use factor_through_squash. { apply setproperty. } cbn ; intros H. induction H as [ k [ p q ]]. rewrite p, q. apply idpath. - use less_than_dcpo_lub. + exact i. + apply refl_dcpo. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous