Definition directed_complete_poset {X : hSet} (PX : PartialOrder X) : UU := ∏ (I : UU) (f : I → X), is_directed PX f → lub PX f.
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.