fact: Definition ExtensionAlong@{a b p m} {A : Type@{a}} {B : Type@{b}} (f : A -> B) (P : B -> Type@{p}) (d : forall x:A, P (f x)) := sig@{m m} (fun (s : forall y:B, P y) => forall x:A, s (f x) = d x).
imports: HoTT.Basics HoTT.Types Equiv.PathSplit PathAny Cubical.DPath Cubical.DPathSquare Colimits.Coeq Colimits.MappingCylinder