fact: Definition isidem_isqidem {X : Type} (f : X -> X) `{IsQuasiIdempotent _ f} : IsIdempotent f := Build_IsIdempotent f (split_idem_split f).
imports: HoTT.Basics HoTT.Types HFiber Constant Truncations.Core Modalities.Modality PathAny