Definition is_least_upperbound (x : X) : hProp := (is_upperbound x ∧ ∀ (y : X), is_upperbound y ⇒ PX x y)%logic.
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.