Mercurial > hg > Members > atton > delta_monad
diff agda/laws.agda @ 97:f26a954cd068
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 |
line wrap: on
line diff
--- a/agda/laws.agda Tue Jan 20 16:25:53 2015 +0900 +++ b/agda/laws.agda Tue Jan 20 16:27:55 2015 +0900 @@ -4,33 +4,34 @@ module laws where -record Functor {l : Level} (F : Set l -> Set l) : (Set (suc l)) where +record Functor {l : Level} (F : {l' : Level} -> Set l' -> Set l') : Set (suc l) where field fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B) field preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x + open Functor +record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l') + {fmapF : {A B : Set l} -> (A -> B) -> (F A) -> (F B)} + {fmapG : {A B : Set l} -> (A -> B) -> (G A) -> (G B)} + (natural-transformation : {A : Set l} -> F A -> G A) + : Set (suc l) where + field + commute : {A B : Set l} -> (f : A -> B) -> (x : F A) -> + natural-transformation (fmapF f x) ≡ fmapG f (natural-transformation x) +open NaturalTransformation -record NaturalTransformation {l : Level} (F G : Set l -> Set l) - (functorF : Functor F) - (functorG : Functor G) : Set (suc l) where - field - natural-transformation : {A : Set l} -> F A -> G A - field - commute : ∀ {A B} -> (f : A -> B) -> (x : F A) -> - natural-transformation (fmap functorF f x) ≡ fmap functorG f (natural-transformation x) -open NaturalTransformation -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f. record Monad {l : Level} {A : Set l} (M : {ll : Level} -> Set ll -> Set ll) - (functorM : Functor M) + (functorM : Functor {l} M) : Set (suc l) where field -- category mu : {A : Set l} -> M (M A) -> M A @@ -43,4 +44,4 @@ left-unity-law : (x : M A) -> (mu ∙ (fmap functorM eta)) x ≡ id x right-unity-law : (x : M A) -> id x ≡ (mu ∙ eta) x -open Monad +open Monad \ No newline at end of file