split_idem_retract' `{fs : Funext} {X : Type} : QuasiIdempotent X -> RetractOf X := fun f => split_idem_retract f.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.