Definition compact_basis_laws (B : dcpo_basis_data X) : UU := (∏ (b : B), is_compact_el (B b)) × (∏ (x : X), is_directed X (compact_basis_le_map B x)) × (∏ (x : X), is_least_upperbound X (compact_basis_le_map B x) x).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Basis.Algebraic. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis.