fact: Definition set_coproduct_scott_continuous_map {Z : dcpo} (f : ∏ (x : X), scott_continuous_map (Y x) Z) : scott_continuous_map coproduct_set_dcpo Z := (λ xy, f (pr1 xy) (pr2 xy)) ,, is_scott_continuous_set_coproduct_map (λ x, pr2 (f x)).
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