{X : Type} (f : X -> X) `{IsQuasiIdempotent _ f} {g : X -> X} (p : f == g) : @IsQuasiIdempotent X g (ispreidem_homotopic f p). Proof. intros x; unfold isidem; simpl. Open Scope long_path_scope. rewrite (concat_Ap (fun x => (p x)^) (p x)^). rewrite !ap_pp, !concat_pp_p; apply whiskerL. rewrite !concat_p_pp; apply moveL_pM. rewrite (concat_pA_p (fun x => (p x)^) (p x)). rewrite (concat_pA_p (fun x => (p x)^) (isidem _ x)). rewrite (concat_Ap (fun x => (p x)^) (ap f (p x)^)). rewrite !concat_pp_p; apply whiskerL. rewrite !ap_V; apply moveR_Vp. rewrite <- ap_compose. rewrite isidem2; try exact _. symmetry; refine (concat_Ap (isidem f) (p x)). Close Scope long_path_scope. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.