Definition dcpowithbottom_ofdcpomorphisms (D D' : dcpowithbottom) : dcpowithbottom. Proof. exists (dcpoofdcpomorphisms D D'). set (leastD' := dcpowithbottom_bottom D'). set (l := const_dcpomor D D' leastD'). exists l. intro f. simpl. intro d. apply dcpowithbottom_isMinimal. Defined.
Require Import UniMath.Foundations.All.