Theorem Bourbaki_Witt_fixpoint : LEM -> ∏ P : Poset, is_chain_complete P -> Bourbaki_Witt_property P. Proof. intros H_LEM P P_CC f. set (is_f_closed := (fun A => (∀ y, A y ⇒ A (f y))) : hsubtype P -> hProp). set (is_chain_closed := (fun A => (∀ C' : Chain_hsubtype P, (∏ y:C', A (pr1 y)) ⇒ A (P_CC C'))) : hsubtype P -> hProp). set (C := (fun x => ∀ A : hsubtype P, is_f_closed A ⇒ is_chain_closed A ⇒ A x) : hsubtype P). assert (C_f_closed : is_f_closed C). { intros x C_x A A_f_closed A_chain_closed. use A_f_closed. use C_x; assumption. } assert (C_chain_closed : is_chain_closed C). { intros x C_x A A_f_closed A_chain_closed. use A_chain_closed. intro; use C_x; assumption. } assert (C_induction : ∀ (A : hsubtype P), is_f_closed (A ∩ C) ⇒ is_chain_closed (A ∩ C) ⇒ C ⊆ A). { intros A A_chain_closed A_f_closed x Cx. apply (Cx (fun x => A x ∧ C x)); assumption. } assert (C_is_chain : is_chain (pr1carrier C)). 2: { set (C_Chain := (C,, C_is_chain) : Chain_hsubtype P). exists (P_CC C_Chain). apply isantisymm_posetRelation. 2: { use progressive_property. } refine (least_upper_bound_is_upper_bound (P_CC _) (_,,_)). use C_f_closed. use C_chain_closed. intros [? ?]; assumption. } set (is_bottleneck := (fun x => ∀ y, C y ⇒ y ≤ x ⇒ (f y ≤ x) ∨ (y = x)) : hsubtype P). assert (bottleneck_comparison : ∀ x, C x ⇒ is_bottleneck x ⇒ ∀ y, C y ⇒ (y ≤ x) ∨ (f x ≤ y)). { intros x C_x x_bottleneck. use C_induction. - intros y [y_comp C_y]. split. 2: { use C_f_closed; assumption. } apply (hconjtohdisj' y_comp). 2: { intros leq_fx_y. apply hdisj_in2. eapply istrans_posetRelation; try eassumption. use progressive_property. } intros leq_y_x. use (hdisj_monot' (x_bottleneck y _ _)); try assumption. + intro; assumption. + intro e_yx; destruct e_yx; apply isrefl_posetRelation. - intros C' IH_C'. split. 2: { use C_chain_closed; intros; apply IH_C'. } destruct (H_LEM (∃ y, C' y ∧ f x ≤ y)) as [C'_passes_fx | C'_notpasses_fx ]. + apply hdisj_in2. refine (factor_through_squash_hProp _ _ C'_passes_fx); intros [y [C'_y leq_fx_y]]. eapply istrans_posetRelation; try eassumption. use least_upper_bound_subtype_is_upper_bound; assumption. + apply hdisj_in1. apply least_upper_bound_univ. intros [y C'_y]. eapply hdisjtoimpl. apply hdisj_comm, IH_C'. intros leq_fx_y. apply C'_notpasses_fx. apply hinhpr; exists y. split; assumption. } assert (all_C_bottleneck : forall x, C x ⇒ is_bottleneck x). { use C_induction. - intros x [x_bottleneck C_x]. split. 2: { use C_f_closed; assumption. } intros y C_y le_y_fx. use (hconjtohdisj' (bottleneck_comparison x _ _ y _)); try assumption. 2: { intro. apply hdisj_in2, isantisymm_posetRelation; assumption. } intro le_yx. apply hdisj_in1. use (hconjtohdisj' (x_bottleneck y _ _)); try assumption. + intro. eapply istrans_posetRelation; try eassumption. use progressive_property. + intros e_yx; destruct e_yx. apply isrefl_posetRelation. - intros C' IH_C'. split. 2: { use C_chain_closed; intros; apply IH_C'. } intros x C_x le_x_supC'. destruct (H_LEM (∃ y, C' y ∧ f x ≤ y)) as [ C'_passes_fx | C'_notpasses_fx ]. { apply hdisj_in1. refine (factor_through_squash_hProp _ _ C'_passes_fx); intros [y [? ?]]. eapply istrans_posetRelation; eauto using least_upper_bound_subtype_is_upper_bound. } apply hdisj_in2. apply isantisymm_posetRelation; try assumption. apply least_upper_bound_subtype_univ. intros y C'_y. destruct (IH_C' (y,,C'_y)) as [y_bottleneck C_y]. use (hconjtohdisj' (bottleneck_comparison y _ _ x _)); try assumption. 2: { intro. eapply istrans_posetRelation; try eassumption. use progressive_property. } intro le_x_y. apply isrefl'_posetRelation, pathsinv0. refine (hdisjtoimpl (y_bottleneck x C_x _) _); try assumption. use (negexists_to_forallneg_restricted C'_notpasses_fx); assumption. } intros [x Cx] [y Cy]; simpl pr1carrier. assert (comparison : x ≤ y ∨ f y ≤ x). { use bottleneck_comparison; try apply all_C_bottleneck; assumption. } apply (hdisj_monot' comparison). { intro; assumption. } intro. eapply istrans_posetRelation; try eassumption. use progressive_property. 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.