lift_extensionalong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} {A : Type@{amin}} {B : Type@{bmin}} (f : A -> B) (P : B -> Type@{pmin}) (d : forall x:A, P (f x)) : ExtensionAlong@{a1 b1 p1 m1} f P d -> ExtensionAlong@{a2 b2 p2 m2} f P d. Proof. intros ext. assert (e2 := ext.2); set (e1 := ext.1) in e2. cbn in e2. exact (e1;e2). 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.