fact: Definition comp_scott_continuous_map {X Y Z : dcpo} (f : scott_continuous_map X Y) (g : scott_continuous_map Y Z) : scott_continuous_map X Z := (λ x, g(f x)) ,, comp_is_scott_continuous (pr2 f) (pr2 g).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness