NaturalIsomorphism I_posttensor 1. Close Scope functor_scope. Variable alpha : associator. Variable lambda : left_unitor. Variable rho : . Notation alpha_nat_trans := ((@morphism_isomorphic (C * (C * C) -> C)%category right_assoc left_assoc) alpha). Notation lambda_nat_trans := ((@morphism_isomorphic _ _ _) lambda). Notation rho_nat_trans := ((@morphism_isomorphic _ _ _) rho). Section coherence_laws. Variable a b c d : C. Local P1 : (a ⊗ (b ⊗ (c ⊗ d))) --> (a ⊗ ((b ⊗ c) ⊗ d)). Proof. apply (morphism_of tensor); split; simpl. - exact (Core.identity a). - exact (alpha_nat_trans (b, (c, d))). 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.