fact: Definition split_idem_retract' `{fs : Funext} {X : Type} : QuasiIdempotent X -> RetractOf X := fun f => split_idem_retract f.
imports: HoTT.Basics HoTT.Types HFiber Constant Truncations.Core Modalities.Modality PathAny