proposition: Lemma dcpomorphism_preserveslub {D D' : dcpo} (f : dcpomorphism D D') {I : UU} {u : I -> D} : isdirected u -> preserveslub f u.
proof: Proof. intro isdirec. apply (pr2 (pr2 f)). exact isdirec. Qed.
imports: UniMath.Foundations.All