Definition dcppo_struct_funspace {X Y : hSet} (DX : dcppo_struct X) (DY : dcppo_struct Y) : dcppo_struct (scott_continuous_map_hSet (X ,, pr1 DX) (Y ,, pr1 DY)). Proof. refine (dcpo_struct_funspace DX DY ,, _). simple refine ((_ ,, _) ,, _). - exact (λ _, pr12 DY). - apply is_scott_continuous_constant. - intros f x ; cbn. apply (pr22 DY). Defined.
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.