Mercurial > hg > Members > atton > delta_monad

comparison agda/laws.agda @ 97:f26a954cd068

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update Natural Transformation definitions
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 20 Jan 2015 16:27:55 +0900
parents bcd4fe52a504
children 9c62373bd474
comparison
equal deleted inserted replaced
96:dfe8c67390bd 97:f26a954cd068
2 open import Level 2 open import Level
3 open import basic 3 open import basic
4 4
5 module laws where 5 module laws where
6 6
7 record Functor {l : Level} (F : Set l -> Set l) : (Set (suc l)) where 7 record Functor {l : Level} (F : {l' : Level} -> Set l' -> Set l') : Set (suc l) where
8 field 8 field
9 fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B) 9 fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B)
10 field 10 field
11 preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x 11 preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x
12 covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) 12 covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A)
13 -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x 13 -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x
14
14 open Functor 15 open Functor
15 16
17 record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l')
18 {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)}
19 {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)}
20 (natural-transformation : {A : Set l} -> F A -> G A)
21 : Set (suc l) where
22 field
23 commute : {A B : Set l} -> (f : A -> B) -> (x : F A) ->
24 natural-transformation (fmapF f x) ≡ fmapG f (natural-transformation x)
25 open NaturalTransformation
16 26
17 27
18 record NaturalTransformation {l : Level} (F G : Set l -> Set l)
19 (functorF : Functor F)
20 (functorG : Functor G) : Set (suc l) where
21 field
22 natural-transformation : {A : Set l} -> F A -> G A
23 field
24 commute : ∀ {A B} -> (f : A -> B) -> (x : F A) ->
25 natural-transformation (fmap functorF f x) ≡ fmap functorG f (natural-transformation x)
26 open NaturalTransformation
27 28
28 29
29 30
30 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f. 31 -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f.
31 record Monad {l : Level} {A : Set l} 32 record Monad {l : Level} {A : Set l}
32 (M : {ll : Level} -> Set ll -> Set ll) 33 (M : {ll : Level} -> Set ll -> Set ll)
33 (functorM : Functor M) 34 (functorM : Functor {l} M)
34 : Set (suc l) where 35 : Set (suc l) where
35 field -- category 36 field -- category
36 mu : {A : Set l} -> M (M A) -> M A 37 mu : {A : Set l} -> M (M A) -> M A
37 eta : {A : Set l} -> A -> M A 38 eta : {A : Set l} -> A -> M A
38 field -- haskell 39 field -- haskell