Mercurial > hg > Members > atton > delta_monad

annotate agda/deltaM/monad.agda @ 104:ebd0d6e2772c

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