(n : nat) {A B C D} (f : A -> B) (g : C -> D) (h : A <~> C) (k : B <~> D) (p : g o h == k o f) : PathSplit n f <~> PathSplit n g. Proof. destruct n as [|n]. 1:apply equiv_idmap. destruct n as [|n]. - simpl. refine (_ *E equiv_contr_contr). refine (equiv_functor_forall' k^-1 _); intros d. unfold hfiber. refine (equiv_functor_sigma' h _); intros a. refine (equiv_concat_l (p a) d oE _). simpl; apply equiv_moveR_equiv_M. - refine (_ oE equiv_pathsplit_isequiv n f). refine ((equiv_pathsplit_isequiv n g)^-1 oE _). apply equiv_iff_hprop; intros e. + refine (isequiv_commsq f g h k (fun a => (p a)^)). + refine (isequiv_commsq' f g h k p). Defined.
Require Import HoTT.Basics HoTT.Types.