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