(f : PreIdempotent X) : RetractOf (IsQuasiIdempotent f). Proof. simple refine (@equiv_retractof' _ (@retractof_equiv' (hfiber (@pr1 _ (fun fi => @IsQuasiIdempotent _ fi.1 fi.2)) f) _ _ (retractof_hfiber retract_retractof_qidem pr1 preidem_retract _ f)) (Splitting_PreIdempotent f) _). - symmetry; refine (hfiber_fibration f _). - intros [[g I] J]; simpl. refine (path_sigma' _ 1 _); simpl. apply path_forall; intros x; apply split_idem_preidem. - simpl; unfold hfiber, Splitting. refine (equiv_sigma_assoc _ _ oE _). apply equiv_functor_sigma_id; intros R; simpl. refine (_ oE (equiv_path_sigma _ _ _)^-1); simpl. refine (equiv_functor_sigma' (equiv_ap10 _ _) _); intros H; simpl. destruct f as [f I]; simpl in *. destruct H; simpl. refine (_ oE (equiv_path_forall _ _)^-1); unfold pointwise_paths. apply equiv_functor_forall_id; intros x; simpl. unfold isidem. apply equiv_concat_l. refine (concat_p1 _ @ concat_1p _). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.