Definition way_below_principal {X : dcpo} (x : X) : UU := ∑ (y : X), y ≪ x.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics.