fact: Definition algebraic_dcpo_struct (X : dcpo) : UU := ∏ (x : X), ∑ (D : directed_set X), (∏ (i : D), is_compact_el (D i)) × is_least_upperbound X D x.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous