{A B A' B'} (f : A -> A') (g : B -> B') (P : A' * B' -> Type) (ef : forall b', ooExtendableAlong f (fun a' => P (a',b'))) (eg : forall a', ooExtendableAlong g (fun b' => P (a',b'))) : ooExtendableAlong (functor_prod f g) P := fun n => extendable_functor_prod n f g P (fun b' => ef b' n) (fun a' => eg a' n).
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.PathSplit Homotopy.IdentitySystems. Require Import Cubical.DPath Cubical.DPathSquare. Require Import Colimits.Coeq Colimits.MappingCylinder.