Definition directed_set_progressive_maps (X : dcpo) : directed_set (monotone_map_dcpo X X). Proof. use make_directed_set. - exact (progressive_map X). - exact (λ f, pr1 f). - exact (is_directed_progressive_maps X). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Examples.Products. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO.