fact: Definition make_dcpo_struct {X : hSet} (PX : PartialOrder X) (HX : directed_complete_poset PX) : dcpo_struct X := PX ,, HX.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets