Mercurial > hg > Members > atton > delta_monad

changeset 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 dfe8c67390bd
children b7f0879e854e
files agda/delta/functor.agda agda/laws.agda
diffstat 2 files changed, 14 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/agda/delta/functor.agda	Tue Jan 20 16:25:53 2015 +0900
+++ b/agda/delta/functor.agda	Tue Jan 20 16:27:55 2015 +0900
@@ -22,7 +22,7 @@
 functor-law-2 f g (mono x)    = refl
 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
 
-delta-is-functor : {l : Level} -> Functor (Delta {l})
+delta-is-functor : {l : Level} -> Functor {l} Delta 
 delta-is-functor = record {  fmap = delta-fmap ;
                              preserve-id = functor-law-1;
                              covariant  = \f g -> functor-law-2 g f}
--- 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