proposition: Lemma ProductFunctor_snd_LaxMonoidal_ap_functor_nat : LaxMonoidalFunctor P → (⨂) ◯ (ProductFunctor_snd P) ∏⟶ (ProductFunctor_snd P) ⟹ ProductFunctor_snd P ◯ (⨂).
proof: Proof. intro L. transform; simpl. - intros [x y]; simpl. exact (snd (bimap (to unit_left) id ∘ transform[@ap_functor_nat _ _ _ _ _ L] ((I, x), (I, y)))). - simpl in *. destruct x as [x1 x2]; destruct y as [y1 y2]; destruct f as [f1 f2]; simpl in *. spose (snd (naturality (@ap_functor_nat _ _ _ _ _ L) (I, x1, (I, x2)) (I, y1, (I, y2)) ((id, f1), (id, f2)))) as X. rewrite comp_assoc. rewrite !bimap_fmap. rewrite snd_comp. rewrite <- bimap_comp. rewrite id_left, id_right. rewrite <- comp_assoc. rewrites. rewrite comp_assoc. rewrite snd_comp. rewrite bimap_fmap. rewrite <- bimap_comp. rewrite bimap_id_id. rewrite id_left, id_right. reflexivity. - simpl in *. destruct x as [x1 x2]; destruct y as [y1 y2]; destruct f as [f1 f2]; simpl in *. spose (snd (naturality (@ap_functor_nat _ _ _ _ _ L) (I, x1, (I, x2)) (I, y1, (I, y2)) ((id, f1), (id, f2)))) as X. rewrite comp_assoc. rewrite !bimap_fmap. rewrite snd_comp. rewrite <- bimap_comp. rewrite id_left, id_right. rewrite <- comp_assoc. rewrites. rewrite comp_assoc. rewrite snd_comp. rewrite bimap_fmap. rewrite <- bimap_comp. rewrite bimap_id_id. rewrite id_left, id_right. reflexivity. 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