(a : A) : ap equiv_split_idem_retract (split_idem_issect (s o r) (equiv_split_idem_retract^-1 a)) @ eisretr equiv_split_idem_retract a = equiv_split_idem_retract_retr (split_idem_sect (s o r) (equiv_split_idem_retract^-1 a)) @ ap r (equiv_split_idem_retract_sect a) @ H a. Proof. simpl. unfold equiv_split_idem_retract_retr, equiv_split_idem_retract_sect. rewrite ap_compose. 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_pp_p; apply moveR_Vp; rewrite !concat_p_pp. do 4 rewrite <- ap_compose. rewrite <- (ap_compose (s o r o s) r (H (r (s a)))). rewrite <- (ap_pp (r o s) _ _). rewrite <- (concat_A1p H (H (r (s a)))). rewrite ap_pp. rewrite <- (ap_compose (r o s) (r o s) _). rewrite !concat_pp_p; apply whiskerL; rewrite !concat_p_pp. rewrite (concat_A1p H (H (r (s a)))). rewrite !concat_pp_p; apply whiskerL. symmetry; refine (concat_A1p H (H a)). 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.