(x : X) : split_idem_splits (s o r) x = ap (split_idem_sect (s o r)) (eissect equiv_split_idem_retract (split_idem_retr (s o r) x))^ @ equiv_split_idem_retract_sect (equiv_split_idem_retract (split_idem_retr (s o r) x)) @ ap s (equiv_split_idem_retract_retr x). Proof. simpl. unfold equiv_split_idem_retract_retr, equiv_split_idem_retract_sect, split_idem_splits. rewrite concat_1p, concat_pp_p, ap_V; apply moveL_Vp; rewrite concat_p1. unfold split_idem_issect, nudge_eq. repeat (rewrite !ap_pp, ?ap_V, !sect_path_split_idem; simpl). unfold isidem; fold A r s H. Open Scope long_path_scope. rewrite !concat_p_pp. rewrite <- !ap_compose; simpl. apply whiskerR. refine (_ @ (concat_1p _)); apply whiskerR. apply moveR_pV; rewrite concat_1p, concat_pp_p; apply moveR_Vp. rewrite <- (ap_compose (s o r o s) (s o r)). rewrite (ap_compose (r o s) s _). rewrite (ap_compose (r o s) s _). rewrite (ap_compose (r o s o r o s) s _). rewrite <- !ap_pp; apply ap. refine (cancelR _ _ (H (r x)) _). rewrite (concat_pA1_p H (H (r x)) _). rewrite (concat_pA1_p H (H (r x)) _). refine ((concat_A1p H (H (r (s (r x)))) @@ 1) @ _). rewrite (ap_compose (r o s) (r o s) _). rewrite (concat_A1p H (ap (r o s) (H (r x)))). rewrite !concat_pp_p; apply whiskerL. symmetry; refine (concat_A1p H (H (r x))). Close Scope long_path_scope. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.