Mercurial > hg > Members > atton > agda-proofs

comparison sandbox/FunctorExample.agda @ 9:4a0841123810

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fmap for nested functor without implicit level
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 18 Jan 2015 20:44:49 +0900
parents a3509dbb9e49
children 7c7659d4521d
comparison
equal deleted inserted replaced
8:a3509dbb9e49 9:4a0841123810
11 _∙_ : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} -> (B -> C) -> (A -> B) -> (A -> C) 11 _∙_ : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} -> (B -> C) -> (A -> B) -> (A -> C)
12 f ∙ g = \x -> f (g x) 12 f ∙ g = \x -> f (g x)
13 13
14 14
15 15
16 record Functor {l : Level} (F : Set l -> Set (suc l)) : (Set (suc l)) where 16 record Functor {l : Level} (F : Set l -> Set l) : (Set (suc l)) where
17 field 17 field
18 fmap : ∀{A B} -> (A -> B) -> (F A) -> (F B) 18 fmap : ∀{A B} -> (A -> B) -> (F A) -> (F B)
19 field 19 field
20 preserve-id : ∀{A} (Fa : F A) → fmap id Fa ≡ id Fa 20 preserve-id : ∀{A} (Fa : F A) → fmap id Fa ≡ id Fa
21 covariant : ∀{A B C} (f : A → B) → (g : B → C) → (x : F A) 21 covariant : ∀{A B C} (f : A → B) → (g : B → C) → (x : F A)
22 → fmap (g ∙ f) x ≡ fmap g (fmap f x) 22 → fmap (g ∙ f) x ≡ fmap g (fmap f x)
23 23
24 data List {l : Level} (A : Set l) : (Set (suc l)) where 24 data List {l : Level} (A : Set l) : (Set l) where
25 nil : List A 25 nil : List A
26 cons : A -> List A -> List A 26 cons : A -> List A -> List A
27 27
28 list-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> List A -> List B 28 list-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> List A -> List B
29 list-fmap f nil = nil 29 list-fmap f nil = nil
37 (f : A -> B) → (g : B -> C) → (x : List A) → list-fmap (g ∙ f) x ≡ list-fmap g (list-fmap f x) 37 (f : A -> B) → (g : B -> C) → (x : List A) → list-fmap (g ∙ f) x ≡ list-fmap g (list-fmap f x)
38 list-covariant f g nil = refl 38 list-covariant f g nil = refl
39 list-covariant f g (cons x xs) = cong (\li -> cons (g (f x)) li) (list-covariant f g xs) 39 list-covariant f g (cons x xs) = cong (\li -> cons (g (f x)) li) (list-covariant f g xs)
40 40
41 41
42 list-is-functor : {l : Level} -> Functor List 42 list-is-functor : {l : Level} -> Functor (List {l})
43 list-is-functor {l} = record { fmap = list-fmap ; 43 list-is-functor = record { fmap = list-fmap ;
44 preserve-id = list-preserve-id ; 44 preserve-id = list-preserve-id ;
45 covariant = list-covariant {l}} 45 covariant = list-covariant}
46 46
47 fmap-to-nest-list : {l ll : Level} {A : Set l} {B : Set l} {fl : {l' : Level} -> Functor {l'} List} 47 fmap-to-nest-list : {l ll : Level} {A : Set l} {B : Set l} {fl : Functor List}
48 -> (A -> B) -> (List (List A)) -> (List (List B)) 48 -> (A -> B) -> (List (List A)) -> (List (List B))
49 fmap-to-nest-list {_} {_} {_} {_} {fl} f xs = Functor.fmap fl (Functor.fmap fl f) xs 49 fmap-to-nest-list {_} {_} {_} {_} {fl} f xs = Functor.fmap fl (Functor.fmap fl f) xs
50 50
51 data Identity {l : Level} (A : Set l) : Set (suc l) where 51 data Identity {l : Level} (A : Set l) : Set l where
52 identity : A -> Identity A 52 identity : A -> Identity A
53 53
54 identity-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> Identity A -> Identity B 54 identity-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> Identity A -> Identity B
55 identity-fmap f (identity a) = identity (f a) 55 identity-fmap f (identity a) = identity (f a)
56 56
59 59
60 identity-covariant : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} -> 60 identity-covariant : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
61 (f : A -> B) → (g : B -> C) → (x : Identity A) → identity-fmap (g ∙ f) x ≡ identity-fmap g (identity-fmap f x) 61 (f : A -> B) → (g : B -> C) → (x : Identity A) → identity-fmap (g ∙ f) x ≡ identity-fmap g (identity-fmap f x)
62 identity-covariant f g (identity x) = refl 62 identity-covariant f g (identity x) = refl
63 63
64 identity-is-functor : {l : Level} -> Functor Identity 64 identity-is-functor : {l : Level} -> Functor (Identity {l})
65 identity-is-functor {l} = record { fmap = identity-fmap {l}; 65 identity-is-functor {l} = record { fmap = identity-fmap {l};
66 preserve-id = identity-preserve-id ; 66 preserve-id = identity-preserve-id ;
67 covariant = identity-covariant } 67 covariant = identity-covariant }
68 68
69 69
70 70
71 71
72 record NaturalTransformation {l ll : Level} (F G : Set l -> Set (suc l)) 72 record NaturalTransformation {l ll : Level} (F G : Set l -> Set l)
73 (functorF : Functor F) 73 (functorF : Functor F)
74 (functorG : Functor G) : Set (suc (l ⊔ ll)) where 74 (functorG : Functor G) : Set (suc (l ⊔ ll)) where
75 field 75 field
76 natural-transformation : {A : Set l} -> F A -> G A 76 natural-transformation : {A : Set l} -> F A -> G A
77 field 77 field