fact: 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).
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