Mercurial > hg > Papers > 2015 > atton-thesis

annotate src/monad_laws.agda @ 43:b7e693b6d7d9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add defintion monad-laws in agda
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 13 Feb 2015 17:51:57 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
43
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 record Monad {l : Level} (T : Set l -> Set l) (F : Functor T)
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 : Set (suc l) where
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 field -- category
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 mu : {A : Set l} -> T (T A) -> T A
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 eta : {A : Set l} -> A -> T A
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 field -- natural transformations
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) ->
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 (eta ∙ f) x ≡ fmap F f (eta x)
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 mu-is-nt : {A B : Set l} -> (f : A -> B) -> (x : T (T A)) ->
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 mu (fmap F (fmap F f) x) ≡ fmap F f (mu x)
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 field -- category laws
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 association-law : {A : Set l} -> (x : (T (T (T A)))) ->
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 (mu ∙ (fmap F mu)) x ≡ (mu ∙ mu) x
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 left-unity-law : {A : Set l} -> (x : T A) ->
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 (mu ∙ (fmap F eta)) x ≡ id x
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 right-unity-law : {A : Set l} -> (x : T A) ->
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 id x ≡ (mu ∙ eta) x
b7e693b6d7d9 Add defintion monad-laws in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21