Proposition is_scott_continuous_inr : is_scott_continuous Y coproduct_dcpo inr. Proof. use make_is_scott_continuous. - apply inr_monotone_function. - intro D ; cbn. use (eq_lub coproduct_dcpo (directed_set_comp (inr_monotone_function X Y) D)). + exact (pr2 (coproduct_dcpo_inr_lub D)). + exact (is_least_upperbound_dcpo_comp_lub _ D). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous.