Definition way_below {X : dcpo} (x y : X) : hProp := (∀ (D : directed_set X), y ⊑ ⨆ D ⇒ ∃ (i : D), x ⊑ D i)%logic.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics.