(X : Type) : Idempotent X <~> RetractOf X. Proof. transitivity ({ f : X -> X & Splitting f }). - unfold Idempotent. refine (equiv_functor_sigma' (equiv_idmap _) _); intros f; simpl. refine (equiv_split_idem_retract (splitting_retractof_isqidem f)). - unfold Splitting. refine (_ oE equiv_sigma_symm _). apply equiv_sigma_contr; intros R. apply contr_basedhomotopy. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.