(f : X -> X) : RetractOf { I : IsPreIdempotent f & IsQuasiIdempotent f }. Proof. simple refine (@equiv_retractof' _ (@retractof_equiv' (hfiber quasiidempotent_pr1 f) _ _ (retractof_hfiber retract_retractof_qidem quasiidempotent_pr1 retract_idem (fun _ => 1) f)) (Splitting f) _). - refine ((hfiber_fibration f (fun g => { I : IsPreIdempotent g & @IsQuasiIdempotent _ g I }))^-1 oE _). unfold hfiber. refine (equiv_functor_sigma' (equiv_sigma_assoc _ _)^-1 (fun a => _)); simpl. destruct a as [[g I] J]; unfold quasiidempotent_pr1; simpl. apply equiv_idmap. - simpl. unfold hfiber, Splitting. refine (equiv_functor_sigma_id _); intros R; simpl. apply equiv_ap10. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.