Definition pointwiseorder (D D' : dcpo) : hrel (dcpomorphism D D'). Proof. intros f g. use make_hProp. - exact (∏ (d : D), f d ≤ g d). - apply impred_isaprop; intro d. apply propproperty. Defined.
Require Import UniMath.Foundations.All.