(X : Type) (f : PreIdempotent X) (ss : forall x, Collapsible (f x = x)) : Splitting f. Proof. simple refine (Build_RetractOf X { x : X & FixedBy (@collapse (f x = x) _) } _ pr1 _ ; _). - intros x; exists (f x); unfold FixedBy. exists (collapse (isidem f x)). apply wconst. - intros [x [p q]]; simpl. apply path_sigma with p. 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.