P3 o P2 o P1 = P5 o P4. Close Scope morphism_scope. Local Q1 : (a ⊗ (I ⊗ b)) --> a ⊗ b. Proof. apply (morphism_of tensor); split; simpl. - exact (Core.identity a). - exact (lambda_nat_trans _). Defined.
Require Import Basics.Utf8. Require Import Category.Core Category.Morphisms. Require Import Functor.Core Require Import NaturalTransformation.Core. Require Import FunctorCategory.Core FunctorCategory.Morphisms. Require Import ProductLaws.