(n : nat) `{f : A -> B} : PathSplit n.+2 f -> IsEquiv f. Proof. intros [g k]. pose (h := fun x y p => (fst (k x y) p).1). pose (hs := fun x y => (fun p => (fst (k x y) p).2) : (ap f) o (h x y) == idmap). clearbody hs; clearbody h; clear k. apply isequiv_contr_map; intros b. apply contr_inhabited_hprop. 2:exact (g b). apply hprop_allpath; intros [a p] [a' p']. refine (path_sigma' _ (h a a' (p @ p'^)) _). refine (transport_paths_Fl _ _ @ _). refine ((inverse2 (hs a a' (p @ p'^)) @@ 1) @ _). refine ((inv_pp p p'^ @@ 1) @ _). refine (concat_pp_p _ _ _ @ _). refine ((1 @@ concat_Vp _) @ _). exact ((inv_V p' @@ 1) @ concat_p1 _). Defined.
Require Import HoTT.Basics HoTT.Types.