(n : nat) {A B C : Type} (P : C -> Type) (f : A -> B) (g : B -> C) : ExtendableAlong n g P -> ExtendableAlong n (g o f) P -> ExtendableAlong n f (fun b => P (g b)). Proof. revert P; simple_induction n n IHn; intros P extg extgf; [ exact tt | split ]. - intros h. exists ((fst extgf h).1 oD g); intros a. exact ((fst extgf h).2 a). - intros h k. pose (h' := (fst extg h).1). pose (k' := (fst extg k).1). refine (extendable_postcompose' n (fun b => h' (g b) = k' (g b)) (fun b => h b = k b) f _ _). + intros b. exact (equiv_concat_lr ((fst extg h).2 b)^ ((fst extg k).2 b)). + apply (IHn (fun c => h' c = k' c) (snd extg h' k') (snd extgf 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.