Proposition const_lub {X : dcpo} (x : X) (I : UU) (i : ∥ I ∥) : ⨆ (const_directed_set X x I i) = x. Proof. use antisymm_dcpo. - use dcpo_lub_is_least. intro j ; cbn. apply refl_dcpo. - revert i. use factor_dep_through_squash. { intro i. apply propproperty. } intro i ; cbn. use less_than_dcpo_lub. + exact i. + cbn. apply refl_dcpo. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.