Definition dcpomorphism_posetmorphism (D D' : dcpo) : dcpomorphism D D' -> posetmorphism D D'. Proof. intros [f isdcpomor]. exists f. exact (pr1 isdcpomor). Defined.
Require Import UniMath.Foundations.All.