fact: Definition make_directed_set {X : hSet} (PX : PartialOrder X) (I : UU) (D : I → X) (HD : is_directed PX D) : directed_set PX := I ,, (D ,, HD).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions