Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.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 9c62373bd474
children ebd0d6e2772c
comparison
equal deleted inserted replaced
102:9c62373bd474 103:a271f3ff1922
16 16
17 17
18 postulate deltaM-mu-is-natural-transformation : {l : Level} {A : Set l} 18 postulate deltaM-mu-is-natural-transformation : {l : Level} {A : Set l}
19 {M : {l' : Level} -> Set l' -> Set l'} -> 19 {M : {l' : Level} -> Set l' -> Set l'} ->
20 {functorM : {l' : Level} -> Functor {l'} M} 20 {functorM : {l' : Level} -> Functor {l'} M}
21 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M (functorM ) } -> 21 {monadM : {l' : Level} -> Monad {l'} M (functorM ) } ->
22 NaturalTransformation (\A -> DeltaM M (DeltaM M A)) (\A -> DeltaM M A) 22 NaturalTransformation (\A -> DeltaM M (DeltaM M A)) (\A -> DeltaM M A)
23 {deltaM-fmap ∙ deltaM-fmap} {deltaM-fmap {l}} 23 {deltaM-fmap ∙ deltaM-fmap} {deltaM-fmap {l}}
24 (deltaM-mu {_} {_} {M} {functorM} {monadM}) 24 (deltaM-mu {_} {_} {M} {functorM} {monadM})
25 25
26 headDeltaM-commute : {l : Level} {A B : Set l} 26 headDeltaM-commute : {l : Level} {A B : Set l}
27 {M : {l' : Level} -> Set l' -> Set l'} -> 27 {M : {l' : Level} -> Set l' -> Set l'} ->
28 {functorM : {l' : Level} -> Functor {l'} M} -> 28 {functorM : {l' : Level} -> Functor {l'} M} ->
29 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M (functorM ) } -> 29 {monadM : {l' : Level} -> Monad {l'} M (functorM ) } ->
30 (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A) -> 30 (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A) ->
31 headDeltaM (deltaM-fmap f x) ≡ fmap functorM f (headDeltaM x) 31 headDeltaM (deltaM-fmap f x) ≡ fmap functorM f (headDeltaM x)
32 headDeltaM-commute f (deltaM (mono x)) = refl 32 headDeltaM-commute f (deltaM (mono x)) = refl
33 headDeltaM-commute f (deltaM (delta x d)) = refl 33 headDeltaM-commute f (deltaM (delta x d)) = refl
34 34
35 35
36 headDeltaM-is-natural-transformation : {l : Level} {A : Set l} 36 headDeltaM-is-natural-transformation : {l : Level} {A : Set l}
37 {M : {l' : Level} -> Set l' -> Set l'} -> 37 {M : {l' : Level} -> Set l' -> Set l'} ->
38 {functorM : {l' : Level} -> Functor {l'} M} 38 {functorM : {l' : Level} -> Functor {l'} M}
39 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM } -> 39 {monadM : {l' : Level} -> Monad {l'} M functorM } ->
40 NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A) M 40 NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A) M
41 {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))} {fmap functorM} headDeltaM 41 {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))} {fmap functorM} headDeltaM
42 -- {deltaM-fmap} {fmap (functorM {l} {A})} headDeltaM 42 -- {deltaM-fmap} {fmap (functorM {l} {A})} headDeltaM
43 headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute } 43 headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute }
44 44
45 headDeltaM-to-mono : {l : Level} {A : Set l}
46 {M : {l' : Level} -> Set l' -> Set l'}
47 {functorM : {l' : Level} -> Functor {l'} M}
48 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
49 -> (x : M A) ->
50 headDeltaM {l} {A} {M} {functorM} {monadM} (deltaM (mono x)) ≡ x
51 headDeltaM-to-mono x = refl
52
53 45
54 deltaM-right-unity-law : {l : Level} {A : Set l} 46 deltaM-right-unity-law : {l : Level} {A : Set l}
55 {M : {l' : Level} -> Set l' -> Set l'} 47 {M : {l' : Level} -> Set l' -> Set l'}
56 (functorM : {l' : Level} -> Functor {l'} M) 48 (functorM : {l' : Level} -> Functor {l'} M)
57 (monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM) 49 (monadM : {l' : Level} -> Monad {l'} M functorM)
58 -> (d : DeltaM M {functorM} {monadM} A) -> 50 (d : DeltaM M {functorM} {monadM} A) ->
59 (deltaM-mu ∙ deltaM-eta) d ≡ id d 51 (deltaM-mu ∙ deltaM-eta) d ≡ id d
60
61
62
63
64 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (mono x)) = begin 52 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (mono x)) = begin
65 (deltaM-mu ∙ deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ 53 (deltaM-mu ∙ deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩
66 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ 54 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
67 deltaM-mu (deltaM (mono (eta monadM (deltaM (mono x))))) ≡⟨ refl ⟩ 55 deltaM-mu (deltaM (mono (eta monadM (deltaM (mono x))))) ≡⟨ refl ⟩
68 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x)))))) ≡⟨ refl ⟩ 56 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x)))))) ≡⟨ refl ⟩
69 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x)))))) 57 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x))))))
70 ≡⟨ cong (\de -> deltaM (mono (mu monadM de))) (sym (eta-is-nt monadM headDeltaM (deltaM (mono x)))) ⟩ 58 ≡⟨ cong (\de -> deltaM (mono (mu monadM de))) (sym (eta-is-nt monadM headDeltaM (deltaM (mono x)))) ⟩
71 deltaM (mono (mu monadM (eta monadM (headDeltaM {l} {A} {M} {functorM} {monadM} (deltaM (mono x)))))) 59 deltaM (mono (mu monadM (eta monadM (headDeltaM {l} {A} {M} {functorM} {monadM} (deltaM (mono x))))))
72 ≡⟨ cong (\de -> deltaM (mono (mu monadM (eta monadM de)))) (headDeltaM-to-mono {l} {A} {M} {functorM} {monadM} x) ⟩ 60 ≡⟨ refl ⟩
73 deltaM (mono (mu monadM (eta {l} {DeltaM M A} monadM x))) 61 deltaM (mono (mu monadM (eta {l} monadM x)))
74 ≡⟨ {!!} ⟩
75 deltaM (mono (mu monadM (eta {l} {A} monadM x)))
76 ≡⟨ cong (\x -> deltaM (mono x)) (sym (right-unity-law monadM x)) ⟩ 62 ≡⟨ cong (\x -> deltaM (mono x)) (sym (right-unity-law monadM x)) ⟩
77 deltaM (mono x) ≡⟨ refl ⟩ 63 deltaM (mono x)
64 ≡⟨ refl ⟩
78 id (deltaM (mono x)) 65 id (deltaM (mono x))
79 ∎ 66 ∎
80 67 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (delta x d)) = begin
81 deltaM-right-unity-law functorM monadM (deltaM (delta x d)) = {!!} 68 (deltaM-mu ∙ deltaM-eta) (deltaM (delta x d)) ≡⟨ refl ⟩
69 deltaM-mu (deltaM-eta (deltaM (delta x d))) ≡⟨ refl ⟩
70 deltaM-mu (deltaM (mono (eta monadM (deltaM (delta x d))))) ≡⟨ refl ⟩
71 deltaM (mono (mu monadM (fmap functorM headDeltaM (eta monadM (deltaM (delta x d))))))
72 ≡⟨ cong (\de -> deltaM (mono (mu monadM de))) (sym (eta-is-nt monadM headDeltaM (deltaM (delta x d)))) ⟩
73 deltaM (mono (mu monadM (eta monadM (headDeltaM (deltaM (delta x d))))))
74 ≡⟨ refl ⟩
75 deltaM (mono (mu monadM (eta monadM x)))
76 ≡⟨ {!!} ⟩
77 id (deltaM (delta x d))
78 ∎
82 79
83 80
84 {- 81 {-
85 deltaM-association-law : {l : Level} {A : Set l} 82 deltaM-association-law : {l : Level} {A : Set l}
86 {M : {l' : Level} -> Set l' -> Set l'} 83 {M : {l' : Level} -> Set l' -> Set l'}