`{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' := equiv_path_extension ext ext'.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.PathSplit Homotopy.IdentitySystems. Require Import Cubical.DPath Cubical.DPathSquare. Require Import Colimits.Coeq Colimits.MappingCylinder.