Definition make_dcpo_lub {D : dcpo} {I : UU} {f : I -> D} : isdirected f -> D. Proof. intro isdirec. exact (pr1 (dcpoisdirectedcomplete D I f isdirec)). Defined.
Require Import UniMath.Foundations.All.