Definition restriction_to_post_fixpoint {X : dcpo} (f : monotone_function X X) : progressive_map (post_fixpoint_dcpo f). Proof. use make_progressive_map. - simple refine (_ ,, _). + refine (λ x, f (pr1 x) ,, _). abstract (cbn ; apply f ; apply (pr2 x)). + abstract (intros x₁ x₂ p ; cbn ; apply f ; exact p). - abstract (exact (λ x, pr2 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.