{X : Type} (R : RetractOf X) : QuasiIdempotent X := (preidem_retract R ; isqidem_retract R). Global Instance ispreidem_split {X : Type} (f : X -> X) (S : Splitting f) : IsPreIdempotent f. Proof. destruct S as [R p]. refine (ispreidem_homotopic _ p); exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.