Definition make_dcpomorphism {D D' : dcpo} (f : D -> D') (i : isdcpomorphism' f) : dcpomorphism D D'. Proof. exists f. apply preservesdirectedlub_isdcpomorphism. exact i. Defined.
Require Import UniMath.Foundations.All.