proposition: Proposition is_directed_progressive_maps (X : dcpo) : is_directed (monotone_map_dcpo X X) (λ (f : progressive_map X), pr1 f).
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Examples.Products UniMath.OrderTheory.DCPOs.Examples.SubDCPO