proposition: Lemma ProductFunctor_LaxMonoidal_ap_functor_nat : LaxMonoidalFunctor F → LaxMonoidalFunctor G → (⨂) ◯ (F ∏⟶ G) ∏⟶ (F ∏⟶ G) ⟹ F ∏⟶ G ◯ (⨂).
proof: Proof. intros O P. transform. { intros [[x z] [y w]]; split. - exact (transform[ap_functor_nat] (x, y)). - exact (transform[ap_functor_nat] (z, w)). } all:(try destruct x as [[x1 x2] [y1 y2]], y as [[z1 z2] [w1 w2]], f as [[f1a f1b] [f2a f2b]]; try destruct A as [[x z] [y w]]; simpl). - split. + abstract apply (naturality ap_functor_nat (x1, y1)). + abstract apply (naturality ap_functor_nat (x2, y2)). - split. + abstract apply (naturality_sym ap_functor_nat (x1, y1) (z1, w1) (f1a, f2a)). + abstract apply (naturality_sym ap_functor_nat (x2, y2) (z2, w2) (f1b, f2b)). Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Bifunctor Category.Functor.Construction.Product Category.Functor.Structure.Monoidal Category.Structure.Monoidal Category.Structure.Monoidal.Product Category.Structure.Monoidal.Proofs Category.Construction.Product Category.Instance.Fun