fact: Definition ispreidem_homotopic {X : Type} (f : X -> X) `{IsPreIdempotent _ f} {g : X -> X} (p : f == g) : IsPreIdempotent g.
imports: HoTT.Basics HoTT.Types HFiber Constant Truncations.Core Modalities.Modality PathAny