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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness.