Definition least_fixpoint_scott_continuous_map_directed_set (X : dcppo) : directed_set (dcpo_funspace (dcpo_funspace X X) X). Proof. use nat_directed_set. - exact least_fixpoint_scott_continuous_map_on_N. - abstract (intros i f ; simpl ; unfold prodtofuntoprod ; simpl ; use is_monotone_scott_continuous_map ; split ; [ apply is_min_bottom_dcppo | ] ; intro ; apply refl_dcpo). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. 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.Examples.Fixpoints. Require Import UniMath.OrderTheory.DCPOs.Examples.Exponentials. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.