Mercurial > hg > Members > atton > delta_monad

annotate agda/deltaM/functor.agda @ 103:a271f3ff1922

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Delte type dependencie in Monad record for escape implicit type conflict
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 26 Jan 2015 14:08:46 +0900
parents 8d92ed54a94f
children ebd0d6e2772c
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open ≡-Reasoning
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import basic
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import delta
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import delta.functor
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import deltaM
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import laws
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open Functor
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 module deltaM.functor where
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 deltaM-preserve-id : {l : Level} {A : Set l}
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 {M : {l' : Level} -> Set l' -> Set l'}
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 (functorM : {l' : Level} -> Functor {l'} M)
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 93
diff changeset
18 {monadM : {l' : Level} -> Monad {l'} M functorM}
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
19 -> (d : DeltaM M {functorM} {monadM} A) -> deltaM-fmap id d ≡ id d
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 deltaM-preserve-id functorM (deltaM (mono x)) = begin
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 deltaM (mono x) ∎
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 deltaM-preserve-id functorM (deltaM (delta x d)) = begin
92
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
27 deltaM-fmap id (deltaM (delta x d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
28 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
29 deltaM (fmap delta-is-functor (fmap functorM id) (delta x d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
30 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
31 deltaM (delta (fmap functorM id x) (fmap delta-is-functor (fmap functorM id) d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
32 ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))) (preserve-id functorM x) ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
33 deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
34 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
35 appendDeltaM (deltaM (mono x)) (deltaM (fmap delta-is-functor (fmap functorM id) d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
36 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
37 appendDeltaM (deltaM (mono x)) (deltaM-fmap id (deltaM d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
38 ≡⟨ cong (\d -> appendDeltaM (deltaM (mono x)) d) (deltaM-preserve-id functorM (deltaM d)) ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
39 appendDeltaM (deltaM (mono x)) (deltaM d)
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
40 ≡⟨ refl ⟩
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 deltaM (delta x d)
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 ∎
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
44
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 deltaM-covariant : {l : Level} {A B C : Set l} ->
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
46 {M : {l' : Level} -> Set l' -> Set l'}
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
47 (functorM : {l' : Level} -> Functor {l'} M)
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 93
diff changeset
48 {monadM : {l' : Level} -> Monad {l'} M functorM}
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
49 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A) ->
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
50 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
51 deltaM-covariant functorM f g (deltaM (mono x)) = begin
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
52 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
53 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
54 deltaM (mono (fmap functorM (f ∙ g) x)) ≡⟨ cong (\x -> (deltaM (mono x))) (covariant functorM g f x) ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
55 deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x)) ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
56 deltaM-fmap f (deltaM-fmap g (deltaM (mono x))) ∎
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
57 deltaM-covariant functorM f g (deltaM (delta x d)) = begin
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
58 deltaM-fmap (f ∙ g) (deltaM (delta x d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
59 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
60 deltaM (delta-fmap (fmap functorM (f ∙ g)) (delta x d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
61 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
62 deltaM (delta (fmap functorM (f ∙ g) x) (delta-fmap (fmap functorM (f ∙ g)) d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
63 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
64 appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM (delta-fmap (fmap functorM (f ∙ g)) d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
65 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
66 appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM-fmap (f ∙ g) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
67 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-fmap (f ∙ g) (deltaM d))) (covariant functorM g f x) ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
68 appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
69 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
70 appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
71 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
72 appendDeltaM (deltaM (delta-fmap ((fmap functorM f) ∙ (fmap functorM g)) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
73 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
74 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
75 ≡⟨ cong (\de -> appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) de) (deltaM-covariant functorM f g (deltaM d)) ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
76 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
77 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
78 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
79 ∎
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
80
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
81
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
82 deltaM-is-functor : {l : Level} {M : {l' : Level} -> Set l' -> Set l'}
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
83 {functorM : {l' : Level} -> Functor {l'} M }
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 93
diff changeset
84 {monadM : {l' : Level} -> Monad {l'} M functorM}
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
85 -> Functor {l} (DeltaM M {functorM} {monadM})
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
86 deltaM-is-functor {_} {_} {functorM} = record { fmap = deltaM-fmap ;
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
87 preserve-id = deltaM-preserve-id functorM ;
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
88 covariant = (\f g -> deltaM-covariant functorM g f)}