{a a' : split_idem} (p : a.1 == a'.1) (q : forall n, a.2 n @ p n = ap f (p n.+1) @ a'.2 n) : a = a'. Proof. simple refine (path_sigma' _ _ _). - apply path_arrow; intros n. exact (p n). - apply path_forall; intros n. abstract ( rewrite transport_forall_constant; rewrite transport_paths_FlFr; rewrite ap_apply_l, ap10_path_arrow; rewrite (ap_compose (fun b => b n.+1) (fun x => f x) _); rewrite ap_apply_l, ap10_path_arrow; rewrite concat_pp_p; apply moveR_Vp; by symmetry ). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.