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