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