Definition dcpo_struct_funspace {X Y : hSet} (DX : dcpo_struct X) (DY : dcpo_struct Y) : dcpo_struct (scott_continuous_map_hSet (X ,, DX) (Y ,, DY)) := pr2 (dcpo_funspace (X ,, DX) (Y ,, DY)).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.FubiniTheorem. Require Import UniMath.OrderTheory.DCPOs.Core.CoordinateContinuity. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.