Mercurial > hg > Members > kono > Proof > category
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 )