Mercurial > hg > Members > atton > delta_monad

annotate agda/deltaM/monad.agda @ 102:9c62373bd474

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 25 Jan 2015 12:16:34 +0900
parents b7f0879e854e
children a271f3ff1922
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
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import laws
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 module deltaM.monad where
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open Functor
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open NaturalTransformation
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open Monad
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
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 postulate deltaM-mu-is-natural-transformation : {l : Level} {A : Set l}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 {M : {l' : Level} -> Set l' -> Set l'} ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 {functorM : {l' : Level} -> Functor {l'} M}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 {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
22 NaturalTransformation (\A -> DeltaM M (DeltaM M A)) (\A -> DeltaM M A)
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 {deltaM-fmap ∙ deltaM-fmap} {deltaM-fmap {l}}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 (deltaM-mu {_} {_} {M} {functorM} {monadM})
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 headDeltaM-commute : {l : Level} {A B : Set l}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 {M : {l' : Level} -> Set l' -> Set l'} ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 {functorM : {l' : Level} -> Functor {l'} M} ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 {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
30 (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A) ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 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
32 headDeltaM-commute f (deltaM (mono x)) = refl
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 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
34
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 headDeltaM-is-natural-transformation : {l : Level} {A : Set l}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 {M : {l' : Level} -> Set l' -> Set l'} ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 {functorM : {l' : Level} -> Functor {l'} M}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 {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
40 NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A) M
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))} {fmap functorM} headDeltaM
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 -- {deltaM-fmap} {fmap (functorM {l} {A})} headDeltaM
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute }
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
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
45 headDeltaM-to-mono : {l : Level} {A : Set l}
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
46 {M : {l' : Level} -> Set l' -> Set l'}
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
47 {functorM : {l' : Level} -> Functor {l'} M}
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
48 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
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
49 -> (x : M A) ->
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
50 headDeltaM {l} {A} {M} {functorM} {monadM} (deltaM (mono x)) ≡ 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
51 headDeltaM-to-mono x = 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
52
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
53
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
54 deltaM-right-unity-law : {l : Level} {A : Set l}
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
55 {M : {l' : Level} -> Set l' -> Set l'}
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
56 (functorM : {l' : Level} -> Functor {l'} M)
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
57 (monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM)
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
58 -> (d : DeltaM M {functorM} {monadM} A) ->
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
59 (deltaM-mu ∙ deltaM-eta) d ≡ id d
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
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
98
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
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
64 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (mono x)) = begin
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
65 (deltaM-mu ∙ deltaM-eta) (deltaM (mono x)) ≡⟨ 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
66 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ 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
67 deltaM-mu (deltaM (mono (eta monadM (deltaM (mono x))))) ≡⟨ 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
68 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x)))))) ≡⟨ 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
69 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (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
70 ≡⟨ cong (\de -> deltaM (mono (mu monadM de))) (sym (eta-is-nt monadM headDeltaM (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
71 deltaM (mono (mu monadM (eta monadM (headDeltaM {l} {A} {M} {functorM} {monadM} (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
72 ≡⟨ cong (\de -> deltaM (mono (mu monadM (eta monadM de)))) (headDeltaM-to-mono {l} {A} {M} {functorM} {monadM} 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
73 deltaM (mono (mu monadM (eta {l} {DeltaM M A} monadM 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
74 ≡⟨ {!!} ⟩
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
75 deltaM (mono (mu monadM (eta {l} {A} monadM 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
76 ≡⟨ cong (\x -> deltaM (mono x)) (sym (right-unity-law monadM 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
77 deltaM (mono x) ≡⟨ 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
78 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
79 ∎
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
80
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
81 deltaM-right-unity-law functorM monadM (deltaM (delta x d)) = {!!}
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
82
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
83
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
84 {-
98
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 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
86 {M : {l' : Level} -> Set l' -> Set l'}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 (functorM : {l' : Level} -> Functor {l'} M)
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 (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
89 -> (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
90 -> ((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
91 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
92 (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
93 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
94 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
95 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
96 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
97 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
98 (deltaM-mu ∙ deltaM-mu) (deltaM (mono x)) ∎
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 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
100 -}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 {-
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 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
105 {M : {l' : Level} -> Set l' -> Set l'}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 {functorM : {l' : Level} -> Functor {l'} M }
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 {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
108 (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
109 (x : M A) ->
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 (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
111 (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
112 nya = {!!}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 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
115 {M : {l' : Level} -> Set l' -> Set l'}
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 {functorM : {l' : Level} -> Functor {l'} M }
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 {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
118 (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
119 (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
120 {-
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 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
122 (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
123
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 (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
125 (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
126 (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
127 (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
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 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
131 (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
132 (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
133 -- (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
134 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
135 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
136 (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
137 (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
138 ∎
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 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
140 {-
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 begin
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 (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
143 (deltaM-bind (deltaM-bind m f) g)
b7f0879e854e Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 ∎
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 -}