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