fact: Definition qidem_retract {X : Type} (R : RetractOf X) : QuasiIdempotent X := (preidem_retract R ; isqidem_retract R).
imports: HoTT.Basics HoTT.Types HFiber Constant Truncations.Core Modalities.Modality PathAny