(n : nat) {A B A' B'} (f : A -> A') (g : B -> B') (P : A' * B' -> Type) (ef : forall b', ExtendableAlong n f (fun a' => P (a',b'))) (eg : forall a', ExtendableAlong n g (fun b' => P (a',b'))) : ExtendableAlong n (functor_prod f g) P. Proof. revert P ef eg; simple_induction n n IH; intros P ef eg; [ exact tt | split ]. - apply extension_functor_prod. + intros b'; exact (fst (ef b'), fun _ _ => tt). + intros a'; exact (fst (eg a'), fun _ _ => tt). - intros h k; apply IH. + intros b'; apply (snd (ef b')). + intros a'; apply (snd (eg a')). 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.