Definition compact_basis_from_algebraic_struct {X : dcpo} (AX : algebraic_dcpo_struct X) : compact_basis X. Proof. use make_compact_basis. - exact (compact_basis_data_from_algebraic_struct AX). - exact (compact_basis_laws_from_algebraic_struct AX). 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.