Definition algebraic_dcpo_struct_to_continuous {X : dcpo} (AX : algebraic_dcpo_struct X) : continuous_dcpo_struct X. Proof. intro x. refine (compact_approximating_family AX x ,, _ ,, _). - abstract (intro i ; apply compact_approximating_family_way_below). - abstract (apply AX). 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.