Definition const_dcpomor (D E : dcpo) (e : E) : dcpomorphism D E. Proof. use make_dcpomorphism. - exact (λ _, e). - intros I u isdirec v islubv. split. + intro i. simpl. apply isrefl_posetRelation. + intros d' ineqs. apply (@factor_through_squash I). * apply propproperty. * intro i. exact (ineqs i). * exact (isdirected_inhabited isdirec). Defined.
Require Import UniMath.Foundations.All.