fact: 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)).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.FubiniTheorem UniMath.OrderTheory.DCPOs.Core.CoordinateContinuity UniMath.OrderTheory.DCPOs.Examples.BinaryProducts