annotate sandbox/FunctorExample.agda @ 6:90abb3f53c03

Add functor example
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 15 Jan 2015 17:27:25 +0900
parents
children c11c259916b7
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
6
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open ≡-Reasoning
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 module FunctorExample where
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 id : {l : Level} {A : Set l} -> A -> A
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 id x = x
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 _∙_ : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} -> (B -> C) -> (A -> B) -> (A -> C)
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 f ∙ g = \x -> f (g x)
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 record Functor {l : Level} (F : Set l -> Set (suc l)) : (Set (suc l)) where
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 field
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 fmap : ∀{A B} -> (A -> B) -> (F A) -> (F B)
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 field
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 preserve-id : ∀{A} (Fa : F A) → fmap id Fa ≡ id Fa
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 covariant : ∀{A B C} (f : A → B) → (g : B → C) → (x : F A)
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 → fmap (g ∙ f) x ≡ fmap g (fmap f x)
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 data List {l : Level} (A : Set l) : (Set (suc l)) where
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 nil : List A
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 cons : A -> List A -> List A
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 list-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> List A -> List B
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 list-fmap f nil = nil
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 list-fmap f (cons x xs) = cons (f x) (list-fmap f xs)
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 list-preserve-id : {l : Level} {A : Set l} -> (xs : List A) -> list-fmap id xs ≡ id xs
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 list-preserve-id nil = refl
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 list-preserve-id (cons x xs) = cong (\li -> cons x li) (list-preserve-id xs)
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 list-covariant : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 (f : A -> B) → (g : B -> C) → (x : List A) → list-fmap (g ∙ f) x ≡ list-fmap g (list-fmap f x)
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 list-covariant f g nil = refl
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 list-covariant f g (cons x xs) = cong (\li -> cons (g (f x)) li) (list-covariant f g xs)
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 list-is-functor : {l : Level} -> Functor List
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 list-is-functor {l} = record { fmap = list-fmap ;
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 preserve-id = list-preserve-id ;
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 covariant = list-covariant {l}}
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 --open module FunctorWithImplicits {l ll : Level} {F : Set l -> Set ll} {{functorT : Functor F}} = Functor functorT
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 --hoge : ∀{F A} {{Functor F}} -> (Fa : F A) -> Functor.fmap id Fa ≡ id Fa
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 --hoge = {!!}
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 {-
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 record NaturalTransformation {l ll : Level} (F G : Set l -> Set ll) : Set (suc (l ⊔ ll)) where
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 field
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 natural : {A : Set l} -> F A -> G A
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 field
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 lemma : ∀{f } {x : Functor F} -> natural (fmap f x) ≡ f (natural x)
90abb3f53c03 Add functor example
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 -}