Proposition discrete_dcpo_lub {A : hSet} (D : directed_set (discrete_dcpo A)) (i : D) : ⨆ D = D i. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.