Definition algebraic_struct_from_compact_basis {X : dcpo} (B : compact_basis X) : algebraic_dcpo_struct X. Proof. intro x. refine (directed_set_from_compact_basis B x ,, _ ,, _). - intro i. apply is_compact_el_basis. - apply is_least_upperbound_compact_basis. Defined.
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.