proposition: Lemma ProductFunctor_LaxMonoidal_proj1_ap_functor_nat : LaxMonoidalFunctor F ∏⟶ G → (⨂) ◯ F ∏⟶ F ⟹ F ◯ (⨂).
proof: Proof. intros P. transform. { intros [x y]. exact (fst (transform[ap_functor_nat[P]] ((x, I), (y, I)))). } all:(try rename x into x0; try rename y into y0; try destruct x0 as [x y], y0 as [z w], f as [f g]; try destruct A as [x y]; simpl). - exact (fst (naturality (ap_functor_nat[P]) (x, I, (y, I)) (z, I, (w, I)) ((f, id), (g, id)))). - exact (fst (naturality_sym (ap_functor_nat[P]) (x, I, (y, I)) (z, I, (w, I)) ((f, id), (g, id)))). 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