`{Funext} {A B : Type} {f : A -> B} {P : B -> Type} {d : forall x:A, P (f x)} (ext ext' : ExtensionAlong f P d) : (ExtensionAlong f (fun y => pr1 ext y = pr1 ext' y) (fun x => pr2 ext x @ (pr2 ext' x)^)) <~> ext = ext'. Proof. revert ext'. srapply equiv_path_from_contr. { unfold ExtensionAlong; cbn. exists (fun y => 1%path). intros x; symmetry; apply concat_pV. } destruct ext as [g gd]; unfold ExtensionAlong; cbn. refine (contr_sigma_sigma (forall y:B, P y) (fun s => forall x:A, s (f x) = d x) (fun a => g == a) (fun a b c => forall x:A, c (f x) = gd x @ (b x)^) g (fun y:B => idpath (g y))). refine (contr_equiv' {p:g o f == d & gd == p} _). cbn. refine (equiv_functor_sigma_id _); intros p. refine (equiv_functor_forall_id _); intros x; cbn. refine (_ oE equiv_path_inverse _ _). symmetry; apply equiv_moveR_1M. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.PathSplit Homotopy.IdentitySystems. Require Import Cubical.DPath Cubical.DPathSquare. Require Import Colimits.Coeq Colimits.MappingCylinder.