(X : Type) (f : PreIdempotent X) `{WeaklyConstant _ _ f} : Splitting f. Proof. simple refine (Build_RetractOf X (FixedBy f) (fun x => (f x ; isidem f x)) pr1 _ ; _). - intros x; apply path_ishprop. - simpl. intros x; reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.