fact: Definition monotone_map_dcpo (X Y : dcpo) : dcpo := sub_dcpo (funset_dcpo X Y) (λ f, make_hProp (is_monotone X Y f) (isaprop_is_monotone _ _ _)) lub_is_monotone.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Examples.Propositions UniMath.OrderTheory.DCPOs.Examples.SubDCPO