Definition posetofdcpomorphisms (D D' : dcpo) : Poset. Proof. use make_Poset. - use make_hSet. + exact (dcpomorphism D D'). + apply (isofhleveltotal2 2). ++ apply impred_isaset; intro d. apply setproperty. ++ intro f; apply isasetaprop, isaprop_isdcpomorphism. - use make_PartialOrder. + apply pointwiseorder. + apply ispartialorder_pointwiseorder. Defined.
Require Import UniMath.Foundations.All.