Mercurial > hg > Members > atton > agda-proofs

comparison sandbox/FunctorExample.agda @ 6:90abb3f53c03

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add functor example
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 15 Jan 2015 17:27:25 +0900
parents
children c11c259916b7
comparison
equal deleted inserted replaced
5:e8494d175afb 6:90abb3f53c03
1 open import Level
2 open import Relation.Binary.PropositionalEquality
3 open ≡-Reasoning
4
5
6 module FunctorExample where
7
8 id : {l : Level} {A : Set l} -> A -> A
9 id x = x
10
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)
13
14
15
16 record Functor {l : Level} (F : Set l -> Set (suc l)) : (Set (suc l)) where
17 field
18 fmap : ∀{A B} -> (A -> B) -> (F A) -> (F B)
19 field
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)
22 → fmap (g ∙ f) x ≡ fmap g (fmap f x)
23
24 data List {l : Level} (A : Set l) : (Set (suc l)) where
25 nil : List A
26 cons : A -> List A -> List A
27
28 list-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> List A -> List B
29 list-fmap f nil = nil
30 list-fmap f (cons x xs) = cons (f x) (list-fmap f xs)
31
32 list-preserve-id : {l : Level} {A : Set l} -> (xs : List A) -> list-fmap id xs ≡ id xs
33 list-preserve-id nil = refl
34 list-preserve-id (cons x xs) = cong (\li -> cons x li) (list-preserve-id xs)
35
36 list-covariant : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
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
39 list-covariant f g (cons x xs) = cong (\li -> cons (g (f x)) li) (list-covariant f g xs)
40
41
42 list-is-functor : {l : Level} -> Functor List
43 list-is-functor {l} = record { fmap = list-fmap ;
44 preserve-id = list-preserve-id ;
45 covariant = list-covariant {l}}
46
47 --open module FunctorWithImplicits {l ll : Level} {F : Set l -> Set ll} {{functorT : Functor F}} = Functor functorT
48
49
50 --hoge : ∀{F A} {{Functor F}} -> (Fa : F A) -> Functor.fmap id Fa ≡ id Fa
51 --hoge = {!!}
52
53
54 {-
55 record NaturalTransformation {l ll : Level} (F G : Set l -> Set ll) : Set (suc (l ⊔ ll)) where
56 field
57 natural : {A : Set l} -> F A -> G A
58 field
59 lemma : ∀{f } {x : Functor F} -> natural (fmap f x) ≡ f (natural x)
60 -}