(x : X) : ap split_idem_sect (split_idem_issect (split_idem_retr x)) = I x. Proof. unfold split_idem_issect, nudge_eq. repeat (rewrite !ap_pp, ?ap_V, !sect_path_split_idem; simpl). apply moveR_Vp, whiskerR; symmetry; apply J. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.