{A B A' B'} (f : A -> A') (g : B -> B') (P : A' * B' -> Type) (ef : forall b', ExtendableAlong 1 f (fun a' => P (a',b'))) (eg : forall a', ExtendableAlong 1 g (fun b' => P (a',b'))) (s : forall z, P (functor_prod f g z)) : ExtensionAlong (functor_prod f g) P s. Proof. srefine (_;_). - intros [a' b']; revert b'. refine ((fst (eg a') _).1). intros b; revert a'. refine ((fst (ef (g b)) _).1). intros a. exact (s (a,b)). - intros [a b]; cbn. refine ((fst (eg (f a)) _).2 b @ _). exact ((fst (ef (g b)) _).2 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.