Theorem fixpoint_for_monotone_on_dcpo {P : Poset} (P_dir: is_directed_complete P) (f : posetmorphism P P) (x : Postfixedpoint f) : ∑ y : Fixedpoint f, x ≤ y. Proof. revert x. set (postfix_f := (fun x => x ≤ f x) : Subposet P). assert (postfix_dc : is_directed_complete postfix_f). { intros [A A_dir]. use least_upper_bound_in_subposet. { use (isdirected_lub P_dir). assumption. } apply least_upper_bound_univ. intros [[x x_postfix] x_A]. eapply istrans_posetRelation. { apply x_postfix. } apply posetmorphism_property. refine (least_upper_bound_is_upper_bound _ (_,,_)). simple refine (value_in_image _ ((_,,_),,_)); assumption. } set (max_monprog_map := maximal_progressive_endomorphism_on_dcpo postfix_dc). destruct max_monprog_map as [[max_map [max_is_mon max_is_prog]] max_is_max]. transparent assert (f_restr_postfix : (arrow_Poset postfix_f postfix_f)). { intros x. exists (f (pr1 x)). apply posetmorphism_property, postfixedpoint_property. } assert (max_map_gives_fixedpoints : f_restr_postfix ∘ max_map ~ max_map). { intros x; apply isantisymm_posetRelation. 2: { apply postfixedpoint_property. } revert x. refine (max_is_max (_,,_)); split. - refine (@isaposetmorphism_compose _ _ _ max_map _ f_restr_postfix _). { assumption. } intros ? ?; apply (posetmorphism_property f). - refine (@isprogressive_compose _ f_restr_postfix max_map _ _). 2: { assumption. } intro; apply postfixedpoint_property. } intros x. simple refine ((pr1 (max_map x),,_),,_); simpl. - exact (maponpaths _ (max_map_gives_fixedpoints x)). - use max_is_prog. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo. Require Import UniMath.OrderTheory.Posets.Subposets.