{X : Type} (R : RetractOf X) : PreIdempotent X := (retract_idem R ; ispreidem_retract R). Arguments ispreidem_retract / . Arguments / . Global Instance isqidem_retract {X : Type} (R : RetractOf X) : IsQuasiIdempotent (retract_idem R). Proof. destruct R as [A r s H]; intros x; unfold isidem; simpl. refine ((ap_compose _ _ _) @ _). apply ap. refine ((ap_compose _ _ _)^ @ _). refine (cancelR _ _ (H (r x)) _). refine (concat_A1p H (H (r x))). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.