fact: Definition Build_IsIdempotent {X : Type} (f : X -> X) : Splitting f -> IsIdempotent f := (equiv_split_idem_retract (splitting_retractof_isqidem f))^-1.
imports: HoTT.Basics HoTT.Types HFiber Constant Truncations.Core Modalities.Modality PathAny