changeset 770:e5850e68be22

fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 13 Dec 2017 09:20:43 +0900
parents 43138aead09b
children b7a774977345
files monoidal.agda
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/monoidal.agda	Tue Dec 12 10:57:56 2017 +0900
+++ b/monoidal.agda	Wed Dec 13 09:20:43 2017 +0900
@@ -319,7 +319,7 @@
    } where
        _⊗_ : ( a b : Obj Sets ) → Obj Sets
        _⊗_ a b = FObj SetsTensorProduct (a , b )
-       --  association operations
+       --  associative operations
        mα→ : {a b c : Obj Sets} →  Hom Sets ( ( a ⊗ b ) ⊗ c ) ( a ⊗ ( b ⊗ c ) )
        mα→ ((a , b) , c ) =  (a , ( b , c ) )
        mα← : {a b c : Obj Sets} →  Hom Sets ( a ⊗ ( b ⊗ c ) ) ( ( a ⊗ b ) ⊗ c )