{X : Type} (f : X -> X) `{IsPreIdempotent _ f} {g : X -> X} (p : f == g) : IsPreIdempotent g. Proof. intros x; refine (_ @ isidem f x @ p x). refine (_ @ (p (f x))^). apply ap; symmetry; apply p. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.