Definition incl_scott_continuous_map (x : X) : scott_continuous_map (Y x) coproduct_set_dcpo := (λ y, x ,, y) ,, is_scott_continuous_incl 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.