Definition continuous_dcpo_struct (X : dcpo) : UU := ∏ (x : X), ∑ (D : directed_set X), (∏ (i : D), D i ≪ x) × is_least_upperbound X D x.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.