{ua : Univalence} (X : Type) : Contr (Splitting_PreIdempotent (preidem_idmap X)). Proof. refine (contr_equiv' {Y : Type & X <~> Y} _). transitivity { S : Splitting (preidem_idmap X) & forall x : X, (retract_issect S.1) (retract_retr S.1 x) = ap (retract_retr S.1) (S.2 x) }. 1:make_equiv. apply equiv_functor_sigma_id; intros [[Y r s eta] ep]; cbn in *. apply equiv_functor_forall_id; intros x. unfold ispreidem_idmap; simpl. rewrite ap_idmap, !concat_pp_p. refine (equiv_moveR_Vp _ _ _ oE _). rewrite concat_p1, concat_p_pp. refine (equiv_concat_r (concat_1p _) _ oE _). refine (equiv_whiskerR _ _ _ oE _). refine (equiv_moveR_Vp _ _ _ oE _). rewrite concat_p1. pose (isequiv_adjointify s r ep eta). refine (_ oE equiv_ap (ap s) _ _). apply equiv_concat_r. refine (cancelR _ _ (ep x) _). rewrite <- ap_compose. refine (concat_A1p ep (ep x)). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.