fact: Definition directed_set_el {X : hSet} {PX : PartialOrder X} (D : directed_set PX) : ∥ D ∥ := is_directed_el (directed_set_is_directed D).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions