Lemma posetofdcpomorphisms_isdirectedcomplete (D D' : dcpo) : isdirectedcomplete (posetofdcpomorphisms D D'). Proof. intros I F isdirec. exists (make_dcpomorphism (pointwiselub F isdirec) (pointwiselub_isdcpomorphism' F isdirec)). apply pointwiselub_islub. Qed.
Require Import UniMath.Foundations.All.