proposition: Lemma ProductFunctor_Monoidal_proj2_ap_functor_iso : MonoidalFunctor F ∏⟶ G → (⨂) ◯ G ∏⟶ G ≅[[(D ∏ D), K]] G ◯ (⨂).
proof: Proof. intros P. isomorphism. - transform. { intros [x y]. exact (snd (transform[to (ap_functor_iso[P])] ((I, x), (I, y)))). } 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 (snd (naturality (to (ap_functor_iso[P])) (I, x, (I, y)) (I, z, (I, w)) ((id, f), (id, g)))). + exact (snd (naturality_sym (to (ap_functor_iso[P])) (I, x, (I, y)) (I, z, (I, w)) ((id, f), (id, g)))). - transform. { intros [x y]. exact (snd (transform[from (ap_functor_iso[P])] ((I, x), (I, y)))). } 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 (snd (naturality (from (ap_functor_iso[P])) (I, x, (I, y)) (I, z, (I, w)) ((id, f), (id, g)))). + exact (snd (naturality_sym (from (ap_functor_iso[P])) (I, x, (I, y)) (I, z, (I, w)) ((id, f), (id, g)))). - destruct x; simpl. apply (iso_to_from (ap_functor_iso[P]) (I, o, (I, o0))). - destruct x; simpl. apply (iso_from_to (ap_functor_iso[P]) (I, o, (I, o0))). 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