proposition: Lemma isaprop_isdcpomorphism {D D' : dcpo} (f : D -> D') : isaprop (isdcpomorphism f).
proof: Proof. apply isapropdirprod. - apply isaprop_isaposetmorphism. - apply impred_isaprop; intro I. apply impred_isaprop; intro u. apply isapropimpl; apply isaprop_preserveslub. Qed.
imports: UniMath.Foundations.All