proposition: Proposition is_scott_continuous_inr : is_scott_continuous Y coproduct_dcpo inr.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous