proposition: Lemma ProductFunctor_Traversable_ap_functor_nat : Traversable F → Traversable G → ∀ H : C ⟶ C, @Applicative _ _ H → (F :*: G) ◯ H ⟹ H ◯ (F :*: G).
proof: Proof. intros O P ??. transform. - simpl. intro x. exact (lax_ap[H0] ∘ bimap (transform[@sequence _ _ _ O _ X] x) (transform[@sequence _ _ _ P _ X] x)). - unfold lax_ap. spose (naturality[@ap_functor_nat _ _ _ _ H0 _] (F x, G x) (F y, G y) (fmap[F] f, fmap[G] f)) as X2. rewrite comp_assoc. rewrites. rewrite <- !comp_assoc. pose proof (naturality[@sequence _ _ _ O _ X] _ _ f) as X3; simpl in *. pose proof (naturality[@sequence _ _ _ P _ X] _ _ f) as X4; simpl in *. rewrite !comp_assoc. comp_left. rewrite bimap_fmap. rewrite <- !bimap_comp. rewrite X3, X4. reflexivity. - unfold lax_ap. spose (naturality[@ap_functor_nat _ _ _ _ H0 _] (F x, G x) (F y, G y) (fmap[F] f, fmap[G] f)) as X2. rewrite comp_assoc. rewrites. rewrite <- !comp_assoc. pose proof (naturality[@sequence _ _ _ O _ X] _ _ f) as X3; simpl in *. pose proof (naturality[@sequence _ _ _ P _ X] _ _ f) as X4; simpl in *. rewrite !comp_assoc. comp_left. rewrite bimap_fmap. rewrite <- !bimap_comp. rewrite X3, X4. reflexivity. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Bifunctor Category.Functor.Product Category.Structure.Monoidal.Closed Category.Structure.Monoidal.Internal.Product Category.Functor.Structure.Monoidal Category.Functor.Traversable Category.Functor.Applicative