RetractOf (QuasiIdempotent X). Proof. refine (Build_RetractOf (QuasiIdempotent X) (RetractOf X) split_idem_retract' qidem_retract _). intros R. exact (@path_retractof _ _ (split_idem_retract' (qidem_retract R)) R (equiv_split_idem_retract R) (equiv_split_idem_retract_retr R) (equiv_split_idem_retract_sect R) (equiv_split_idem_retract_issect R)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.