proposition: Proposition comp_is_scott_continuous {X Y Z : hSet} {DX : dcpo_struct X} {DY : dcpo_struct Y} {DZ : dcpo_struct Z} {f : X → Y} {g : Y → Z} (Df : is_scott_continuous DX DY f) (Dg : is_scott_continuous DY DZ g) : is_scott_continuous DX DZ (λ x, g(f x)).
proof: Proof. split. - intros x₁ x₂ p. apply (is_scott_continuous_monotone Dg). apply (is_scott_continuous_monotone Df). exact p. - intros I D HD x Hx. use (is_scott_continuous_lub Dg). + exact (is_directed_comp _ (pr1 Df) HD). + use (is_scott_continuous_lub Df HD). exact Hx. Qed.
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