(a : split_idem (s o r)) : H (r (s (r (split_idem_sect (s o r) a)))) @ H (r (split_idem_sect (s o r) a)) = ap (r o split_idem_sect (s o r)) (ap (split_idem_retr (s o r)) (1 @ ap (split_idem_sect (s o r)) (split_idem_issect (s o r) a)) @ split_idem_issect (s o r) a). Proof. rewrite ap_pp. rewrite <- ap_compose; simpl. rewrite concat_1p. rewrite <- (ap_compose (split_idem_sect (s o r)) (r o s o r) (split_idem_issect (s o r) a)). rewrite (ap_compose _ (r o s o r) (split_idem_issect (s o r) a)). rewrite (ap_compose _ r (split_idem_issect (s o r) a)). unfold split_idem_issect, nudge_eq; repeat (rewrite !ap_pp, ?ap_V, !sect_path_split_idem; simpl). unfold isidem; fold r s H. rewrite !concat_pp_p. rewrite <- !ap_compose. rewrite <- (ap_compose (s o r) r). rewrite <- (ap_compose (s o r) (r o s o r)). rewrite (concat_p_Vp (ap (r o s o r) (a.2 0))). rewrite_moveL_Vp_p. rewrite (ap_compose (r o s o r) (r o s) (a.2 0)). rewrite (concat_A1p H (ap (r o s o r) (a.2 0))). rewrite (ap_compose r (r o s) (a.2 0)). rewrite (concat_pA1_p H (ap r (a.2 0))). apply whiskerR. refine (cancelR _ _ (H (r (a.1 1%nat))) _). rewrite (concat_pA1_p H (H (r (a 1%nat)))). rewrite !concat_pp_p; symmetry; refine (_ @ concat_pp_p _ _ _). exact (concat_A1p (fun x => H (r (s x)) @ H x) (H (r (a 1%nat)))). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.