Mercurial > hg > Members > atton > agda-proofs

changeset 8:a3509dbb9e49

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Example for implicit-level functor
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 18 Jan 2015 20:06:33 +0900
parents c11c259916b7
children 4a0841123810
files sandbox/FunctorExample.agda
diffstat 1 files changed, 4 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/sandbox/FunctorExample.agda	Sat Jan 17 22:13:47 2015 +0900
+++ b/sandbox/FunctorExample.agda	Sun Jan 18 20:06:33 2015 +0900
@@ -44,6 +44,9 @@
                                preserve-id = list-preserve-id ;
                                covariant   = list-covariant {l}}
 
+fmap-to-nest-list : {l ll : Level} {A : Set l} {B : Set l} {fl : {l' : Level} -> Functor {l'} List}
+                    -> (A -> B) -> (List (List A)) -> (List (List B))
+fmap-to-nest-list {_} {_} {_} {_} {fl} f xs = Functor.fmap fl (Functor.fmap fl f)  xs
 
 data Identity {l : Level} (A : Set l) : Set (suc l) where
   identity : A -> Identity A
@@ -86,4 +89,4 @@
 
 tail-is-natural-transformation : {l ll : Level} -> NaturalTransformation  {l} {ll} List List list-is-functor list-is-functor
 tail-is-natural-transformation = record { natural-transformation = tail;
-                                          commute                = tail-commute} 
\ No newline at end of file
+                                          commute                = tail-commute}