{X : Type} (f : X -> X) `{IsQuasiIdempotent _ f} : IsIdempotent f := Build_IsIdempotent f (split_idem_split f). Global Instance ispreidem_isidem {X : Type} (f : X -> X) `{IsIdempotent _ f} : IsPreIdempotent f. Proof. refine (split_idem_sect (retract_idem (splitting_retractof_isqidem f)) _).1. assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.