Lemma maximal_progressive_endomorphism_on_dcpo {P : Poset} (P_DC : is_directed_complete P) : greatest_suchthat (fun f : arrow_Poset P P => isaposetmorphism_hProp f ∧ isprogressive f). Proof. set (mon_prog_maps := (fun f : arrow_Poset P P => isaposetmorphism_hProp f ∧ isprogressive f) : hsubtype _). cut (carrier (is_greatest_suchthat mon_prog_maps)). { intros f. exact (make_greatest_suchthat (pr1 f) (pr2 f)). } cut (carrier (mon_prog_maps ∩ is_least_upper_bound_subtype mon_prog_maps)). { use subtype_inc. intros ? [? ?]. apply greatest_if_contains_sup; assumption. } cut (carrier (is_least_upper_bound_pointwise (@pr1carrier _ mon_prog_maps))). { use subtype_inc. intros f f_pw_lub; split; [ split | ]. - eapply isaposetmorphism_pointwise_lub; try eassumption. intros [g [g_mon g_prog]]; exact g_mon. - eapply progressive_pointwise_lub; try eassumption. { intros [g [g_mon g_prog]]; exact g_prog. } apply hinhpr. exists (idfun _); split. + apply isaposetmorphism_idfun. + apply isprogressive_idfun. - apply is_least_upper_bound_if_pointwise; assumption. } use (foralltototal _ (fun _ y => is_least_upper_bound _ y)). intros x. cut (least_upper_bound (fun g : mon_prog_maps => pr1 g x)). { intros p. exists p. apply least_upper_bound_property. } apply isdirected_lub; try assumption. split. - apply hinhpr. exists (idfun _); split. + apply isaposetmorphism_idfun. + apply isprogressive_idfun. - intros [f [f_mon f_prog]] [g [g_mon g_prog]]. apply hinhpr. use tpair. { exists (f ∘ g); split. + apply isaposetmorphism_compose; assumption. + apply isprogressive_compose; assumption. } split; simpl. + use f_mon; use g_prog. + use f_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.