Theorem Tarski_fixpoint_theorem {P:Poset} (P_complete : is_complete P) (f : posetmorphism P P) : is_complete ((fun x:P => f x = x) : Subposet P). Proof. intros A. set (A_in_P := (fun x:P => ∑ x_fix : (f x = x)%logic, A (x,,x_fix))%prop). set (sup_P_A := P_complete A_in_P). assert (sup_fix_A : least_suchthat (fun x:P => f x = x ∧ sup_P_A ≤ x)). { apply Knaster_Tarski_fixpoint; try assumption. apply least_upper_bound_subtype_univ. intros y [y_fix A_y]. apply (istrans_posetRelation _ _ (f y)). { apply isrefl'_posetRelation, pathsinv0; assumption. } apply posetmorphism_property, least_upper_bound_subtype_is_upper_bound. use tpair; assumption. } assert (sup_A_isfix : f sup_fix_A = sup_fix_A). { apply (least_suchthat_satisfies sup_fix_A). } use make_least_upper_bound. { exists sup_fix_A. assumption. } split. - intros [[x x_fix] A_x]. simpl. apply (istrans_posetRelation _ _ (sup_P_A)). + apply least_upper_bound_subtype_is_upper_bound. use tpair; assumption. + apply (least_suchthat_satisfies sup_fix_A). - intros [[x x_fix] x_ub]. cbn. apply least_suchthat_is_least. split; try assumption. apply least_upper_bound_subtype_univ. intros y [y_fix A_y]. use (x_ub ((_,,_),,_)); assumption. 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.