Mercurial > hg > Members > atton > delta_monad

annotate agda/deltaM/functor.agda @ 92:4d615910c87a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove preserve-id for deltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 14:32:07 +0900
parents f41682b53992
children 8d92ed54a94f
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)
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 -> (d : DeltaM M {functorM} {monadM} A) -> (deltaM-fmap id) d ≡ id d
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
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 {-
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} ->
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 (delta-fmap (f ∙ g)) d ≡ (delta-fmap f) (delta-fmap g d)
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 deltaM-covariant = {!!}
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 -}