lift_extendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} (n : nat) {A : Type@{amin}} {B : Type@{bmin}} (f : A -> B) (P : B -> Type@{pmin}) : ExtendableAlong@{a1 b1 p1 m1} n f P -> ExtendableAlong@{a2 b2 p2 m2} n f P. Proof. revert P; simple_induction n n IH; intros P. - intros _; exact tt. - intros ext; split. + intros g; exact (lift_extensionalong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} _ _ _ (fst ext g)). + intros h k. pose (P' := (fun b => h b = k b) : B -> Type@{pmin}). exact (IH P' (snd ext h k)). 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.