Definition sumof_scott_continuous_maps {Z : dcpo} (f : scott_continuous_map X Z) (g : scott_continuous_map Y Z) : scott_continuous_map coproduct_dcpo Z := sumofmaps f g ,, is_scott_continuous_sumofmaps (pr2 f) (pr2 g).
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.