extendable_postcompose' (n : nat) {A B : Type} (C D : B -> Type) (f : A -> B) (g : forall b, C b <~> D b) : ExtendableAlong n f C -> ExtendableAlong n f D. Proof. generalize dependent C; revert D. simple_induction n n IH; intros C D g; simpl. 1:apply idmap. refine (functor_prod _ _). - refine (functor_forall (functor_forall idmap (fun a => (g (f a))^-1)) _); intros h; simpl. refine (functor_sigma (functor_forall idmap g) _); intros k. refine (functor_forall idmap _); intros a; unfold functor_arrow, functor_forall, composeD; simpl. apply moveR_equiv_M. - refine (functor_forall (functor_forall idmap (fun b => (g b)^-1)) _); intros h. refine (functor_forall (functor_forall idmap (fun b => (g b)^-1)) _); intros k; simpl; unfold functor_forall. refine (IH _ _ _); intros b. apply equiv_inverse, equiv_ap; exact _. 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.