Mercurial > hg > Members > kono > Proof > category
diff applicative.agda @ 773:60942538dc41
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 29 Dec 2017 11:32:19 +0900 |
parents | 43138aead09b |
children | 06388660995b |
line wrap: on
line diff
--- a/applicative.agda Wed Dec 13 09:34:45 2017 +0900 +++ b/applicative.agda Fri Dec 29 11:32:19 2017 +0900 @@ -315,7 +315,7 @@ ---- -- --- Monoidal laws imples Applicative laws +-- Monoidal laws implies Applicative laws -- HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )