Mercurial > hg > Members > atton > delta_monad

annotate agda/deltaM/monad.agda @ 111:9fe3d0bd1149

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove right-unity-law on DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 29 Jan 2015 11:42:22 +0900
parents ebd0d6e2772c
children 0a3b6cb91a05
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
98
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open ≡-Reasoning
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import basic
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import delta
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import delta.functor
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
8 open import delta.monad
98
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import deltaM
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import deltaM.functor
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
11 open import nat
98
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import laws
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 module deltaM.monad where
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open Functor
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open NaturalTransformation
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open Monad
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
102
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
20
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
21 deltaM-right-unity-law : {l : Level} {A : Set l}
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 102
diff changeset
22 {M : {l' : Level} -> Set l' -> Set l'}
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
23 {functorM : {l' : Level} -> Functor {l'} M}
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
24 {monadM : {l' : Level} -> Monad {l'} M functorM}
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
25 {n : Nat}
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
26 (d : DeltaM M {functorM} {monadM} A (S n)) ->
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 102
diff changeset
27 (deltaM-mu ∙ deltaM-eta) d ≡ id d
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
28 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
29 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
30 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
31 deltaM (mono (mu mm (fmap fm (headDeltaM {M = M})(eta mm (deltaM (mono x))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
32 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
33 deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
34 deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
35 deltaM (mono x)
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
36 ∎
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
37 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
38 deltaM-mu (deltaM-eta (deltaM (delta x d)))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
39 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
40 deltaM-mu (deltaM (delta (eta mm (deltaM (delta x d))) (delta-eta (eta mm (deltaM (delta x d))))))
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
41 ≡⟨ refl ⟩
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
42 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (eta mm (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
43 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
44 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de)))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
45 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
46 (sym (eta-is-nt mm headDeltaM (deltaM (delta x d)))) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
47 appendDeltaM (deltaM (mono (mu mm (eta mm ((headDeltaM {monadM = mm}) (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
48 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
49 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
50 appendDeltaM (deltaM (mono (mu mm (eta mm x))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
51 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
52 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
53 (sym (right-unity-law mm x)) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
54 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))
103
a271f3ff1922 Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 102
diff changeset
55 ≡⟨ refl ⟩
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
56 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-eta (eta mm (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
57 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM de))) (sym (eta-is-nt delta-is-monad (fmap fm tailDeltaM) (eta mm (deltaM (delta x d))))) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
58 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (fmap fm tailDeltaM (eta mm (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
59 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta de)))) (sym (eta-is-nt mm tailDeltaM (deltaM (delta x d)))) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
60 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (eta mm (tailDeltaM (deltaM (delta x d)))))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
61 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
62 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (eta mm (deltaM d)))))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
63 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
64 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-eta (deltaM d)))
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
65 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-right-unity-law (deltaM d)) ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
66 appendDeltaM (deltaM (mono x)) (deltaM d)
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
67 ≡⟨ refl ⟩
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
68 deltaM (delta x d)
102
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
69 ∎
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
70
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
71
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
72 {-
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
73 deltaM-left-unity-law : {l : Level} {A : Set l}
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
74 {M : {l' : Level} -> Set l' -> Set l'}
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
75 (functorM : {l' : Level} -> Functor {l'} M)
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
76 (monadM : {l' : Level} -> Monad {l'} M functorM)
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
77 (d : DeltaM M {functorM} {monadM} A (S O)) ->
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
78 (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
79 deltaM-left-unity-law functorM monadM (deltaM (mono x)) = begin
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
80 (deltaM-mu ∙ deltaM-fmap deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
81 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
82 deltaM-mu (deltaM (mono (fmap functorM deltaM-eta x))) ≡⟨ refl ⟩
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
83 deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
84 deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
85
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
86 id (deltaM (mono x))
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
87 ∎
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
88 deltaM-left-unity-law functorM monadM (deltaM (delta x ()))
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
89 -}
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
90
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
91 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
92 {M : {l' : Level} -> Set l' -> Set l'}
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
93 (functorM : {l' : Level} -> Functor {l'} M)
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
94 (monadM : {l' : Level}-> Monad {l'} M functorM) ->
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
95 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) deltaM-is-functor
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
96 deltaM-is-monad functorM monadM = record
111
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
97 { mu = deltaM-mu;
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
98 eta = deltaM-eta;
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
99 return = deltaM-eta;
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
100 bind = deltaM-bind;
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
101 association-law = {!!};
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
102 left-unity-law = {!!};
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
103 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ;
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
104 eta-is-nt = {!!}
9fe3d0bd1149 Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
105 }
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
106
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
107
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
108
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
109
102
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
110
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
111
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
112 {-
98
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 deltaM-association-law : {l : Level} {A : Set l}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 {M : {l' : Level} -> Set l' -> Set l'}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 (functorM : {l' : Level} -> Functor {l'} M)
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 (monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM)
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 -> (d : DeltaM M (DeltaM M (DeltaM M {functorM} {monadM} A)))
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 -> ((deltaM-mu ∙ (deltaM-fmap deltaM-mu)) d) ≡ ((deltaM-mu ∙ deltaM-mu) d)
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 deltaM-association-law functorM monadM (deltaM (mono x)) = begin
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 (deltaM-mu ∙ deltaM-fmap deltaM-mu) (deltaM (mono x)) ≡⟨ refl ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
102
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
122 deltaM-mu (deltaM (delta-fmap (fmap functorM deltaM-mu) (mono x))) ≡⟨ {!!} ⟩
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
123 deltaM-mu (deltaM (mono (bind monadM x headDeltaM))) ≡⟨ refl ⟩
9c62373bd474 Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 98
diff changeset
124 deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
98
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 (deltaM-mu ∙ deltaM-mu) (deltaM (mono x)) ∎
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 deltaM-association-law functorM monadM (deltaM (delta x d)) = {!!}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 -}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 {-
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 nya : {l : Level} {A B C : Set l} ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 {M : {l' : Level} -> Set l' -> Set l'}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 {functorM : {l' : Level} -> Functor {l'} M }
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 (m : DeltaM M {functorM} {monadM} A) -> (f : A -> (DeltaM M {functorM} {monadM} B)) -> (g : B -> (DeltaM M C)) ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 (x : M A) ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 (deltaM (fmap delta-is-functor (\x -> bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))) (mono x))) ≡
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 (deltaM-bind (deltaM (fmap delta-is-functor (\x -> (bind {l} {A} monadM x (headDeltaM ∙ f))) (mono x))) g)
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 nya = {!!}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 deltaM-monad-law-h-3 : {l : Level} {A B C : Set l} ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 {M : {l' : Level} -> Set l' -> Set l'}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 {functorM : {l' : Level} -> Functor {l'} M }
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 (m : DeltaM M {functorM} {monadM} A) -> (f : A -> (DeltaM M B)) -> (g : B -> (DeltaM M C)) ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 (deltaM-bind m (\x -> deltaM-bind (f x) g)) ≡ (deltaM-bind (deltaM-bind m f) g)
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 {-
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 deltaM-monad-law-h-3 {l} {A} {B} {C} {M} {functorM} {monadM} (deltaM (mono x)) f g = begin
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 (deltaM-bind (deltaM (mono x)) (\x -> deltaM-bind (f x) g)) ≡⟨ refl ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))))) ≡⟨ {!!} ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 (deltaM-bind (deltaM (fmap delta-is-functor (\x -> (bind {l} {A} monadM x (headDeltaM ∙ f))) (mono x))) g) ≡⟨ refl ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 (deltaM-bind (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) g) ≡⟨ refl ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 (deltaM-bind (deltaM-bind (deltaM (mono x)) f) g) ∎
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 -}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 deltaM-monad-law-h-3 {l} {A} {B} {C} {M} {functorM} {monadM} (deltaM (mono x)) f g = begin
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 (deltaM-bind (deltaM (mono x)) (\x -> deltaM-bind (f x) g)) ≡⟨ refl ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))))) ≡⟨ {!!} ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 -- (deltaM (fmap delta-is-functor (\x -> bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))) (mono x))) ≡⟨ {!!} ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162 deltaM (mono (bind {l} {B} monadM (bind {_} {A} monadM x (headDeltaM ∙ f)) (headDeltaM ∙ g))) ≡⟨ {!!} ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 deltaM (mono (bind {l} {B} monadM (bind {_} {A} monadM x (headDeltaM ∙ f)) (headDeltaM ∙ g))) ≡⟨ {!!} ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 (deltaM-bind (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) g) ≡⟨ refl ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 (deltaM-bind (deltaM-bind (deltaM (mono x)) f) g)
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166 ∎
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167 deltaM-monad-law-h-3 (deltaM (delta x d)) f g = {!!}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168 {-
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 begin
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170 (deltaM-bind m (\x -> deltaM-bind (f x) g)) ≡⟨ {!!} ⟩
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 (deltaM-bind (deltaM-bind m f) g)
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 ∎
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 -}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 -}