fact: Definition dcpo_lub {X : dcpo} (D : directed_set X) : X := pr22 X _ D (directed_set_is_directed D).
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.DCPOs.Core.DirectedSets