Proposition is_directed_progressive_maps (X : dcpo) : is_directed (monotone_map_dcpo X X) (λ (f : progressive_map X), pr1 f). Proof. split. - apply hinhpr. apply id_progressive_map. - intros f g. apply hinhpr. refine (comp_progressive_map f g ,, _ ,, _). + intro x ; cbn. exact (progressive_map_is_progressive g (f x)). + intro x ; cbn. apply (pr1 g). apply (progressive_map_is_progressive f x). Qed.
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.