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