Definition pointwiselub {D D' : dcpo} {I : UU} (F : I -> posetofdcpomorphisms D D') (isdir : isdirected F) : D -> D'. Proof. intro d. set (ptfamdir := pointwisefamily_isdirected F isdir d). exact (make_dcpo_lub ptfamdir). Defined.
Require Import UniMath.Foundations.All.