{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) : ap split_idem_sect (path_split_idem p q) = p 0. Proof. change (ap ((fun b => b 0) o pr1) (path_split_idem p q) = p 0). refine (ap_compose pr1 (fun b => b 0) _ @ _). refine (ap (ap (fun b => b 0)) (pr1_path_sigma _ _) @ _). refine (ap_apply_l _ 0 @ _). apply ap10_path_arrow. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.