Definition is_algebraic_to_algebraic_struct {X : dcpo} (CX : is_algebraic_dcpo X) : algebraic_dcpo_struct X. Proof. intros x. refine (is_algebraic_dcpo_directed_set CX x ,, _ ,, _). - abstract (intros i ; apply i). - abstract (pose (is_least_upperbound_dcpo_lub (is_algebraic_dcpo_directed_set CX x)) as h ; rewrite (is_algebraic_dcpo_directed_set_lub CX x) in h ; exact h). Defined.
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. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.