Definition make_dcpo_struct {X : hSet} (PX : PartialOrder X) (HX : directed_complete_poset PX) : dcpo_struct X := PX ,, HX.
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.