fact: Definition path_split_idem {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'.
imports: HoTT.Basics HoTT.Types HFiber Constant Truncations.Core Modalities.Modality PathAny