Mercurial > hg > Members > atton > delta_monad
comparison agda/deltaM/monad.agda @ 102:9c62373bd474
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 |
comparison
equal
deleted
inserted
replaced
101:29c54b0197fb | 102:9c62373bd474 |
---|---|
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 | |
45 | 52 |
46 | 53 |
54 deltaM-right-unity-law : {l : Level} {A : Set l} | |
55 {M : {l' : Level} -> Set l' -> Set l'} | |
56 (functorM : {l' : Level} -> Functor {l'} M) | |
57 (monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM) | |
58 -> (d : DeltaM M {functorM} {monadM} A) -> | |
59 (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 | |
65 (deltaM-mu ∙ deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ | |
66 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ | |
67 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 ⟩ | |
69 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)))) ⟩ | |
71 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) ⟩ | |
73 deltaM (mono (mu monadM (eta {l} {DeltaM M A} 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)) ⟩ | |
77 deltaM (mono x) ≡⟨ refl ⟩ | |
78 id (deltaM (mono x)) | |
79 ∎ | |
80 | |
81 deltaM-right-unity-law functorM monadM (deltaM (delta x d)) = {!!} | |
82 | |
83 | |
84 {- | |
47 deltaM-association-law : {l : Level} {A : Set l} | 85 deltaM-association-law : {l : Level} {A : Set l} |
48 {M : {l' : Level} -> Set l' -> Set l'} | 86 {M : {l' : Level} -> Set l' -> Set l'} |
49 (functorM : {l' : Level} -> Functor {l'} M) | 87 (functorM : {l' : Level} -> Functor {l'} M) |
50 (monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM) | 88 (monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM) |
51 -> (d : DeltaM M (DeltaM M (DeltaM M {functorM} {monadM} A))) | 89 -> (d : DeltaM M (DeltaM M (DeltaM M {functorM} {monadM} A))) |
52 -> ((deltaM-mu ∙ (deltaM-fmap deltaM-mu)) d) ≡ ((deltaM-mu ∙ deltaM-mu) d) | 90 -> ((deltaM-mu ∙ (deltaM-fmap deltaM-mu)) d) ≡ ((deltaM-mu ∙ deltaM-mu) d) |
53 deltaM-association-law functorM monadM (deltaM x) = {!!} | |
54 {- | |
55 begin | |
56 (deltaM-mu ∙ deltaM-fmap deltaM-mu) d ≡⟨ refl ⟩ | |
57 deltaM-mu (deltaM-fmap deltaM-mu d) ≡⟨ {!!} ⟩ | |
58 deltaM-mu (deltaM-mu d) ≡⟨ refl ⟩ | |
59 (deltaM-mu ∙ deltaM-mu) d | |
60 ∎ | |
61 -} | |
62 {- | |
63 deltaM-association-law functorM monadM (deltaM (mono x)) = begin | 91 deltaM-association-law functorM monadM (deltaM (mono x)) = begin |
64 (deltaM-mu ∙ deltaM-fmap deltaM-mu) (deltaM (mono x)) ≡⟨ refl ⟩ | 92 (deltaM-mu ∙ deltaM-fmap deltaM-mu) (deltaM (mono x)) ≡⟨ refl ⟩ |
65 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ | 93 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ |
66 deltaM-mu (deltaM (delta-fmap (fmap functorM deltaM-mu) (mono x))) ≡⟨ refl ⟩ | 94 deltaM-mu (deltaM (delta-fmap (fmap functorM deltaM-mu) (mono x))) ≡⟨ {!!} ⟩ |
67 deltaM-mu (deltaM (mono (fmap functorM deltaM-mu x))) ≡⟨ refl ⟩ | 95 deltaM-mu (deltaM (mono (bind monadM x headDeltaM))) ≡⟨ refl ⟩ |
68 deltaM-bind (deltaM (mono (fmap functorM deltaM-mu x))) id ≡⟨ refl ⟩ | 96 deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ |
69 deltaM (mono (bind monadM (fmap functorM deltaM-mu x) (headDeltaM ∙ id))) ≡⟨ refl ⟩ | |
70 deltaM (mono (bind monadM (fmap functorM deltaM-mu x) headDeltaM)) ≡⟨ {!!} ⟩ | |
71 deltaM (mono (bind monadM (bind monadM x headDeltaM) headDeltaM)) ≡⟨ refl ⟩ | |
72 deltaM (mono (bind monadM (bind monadM x (headDeltaM ∙ id)) (headDeltaM ∙ id))) ≡⟨ refl ⟩ | |
73 deltaM-mu (deltaM (mono (bind monadM x (headDeltaM ∙ id)))) ≡⟨ refl ⟩ | |
74 deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ | 97 deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ |
75 (deltaM-mu ∙ deltaM-mu) (deltaM (mono x)) ∎ | 98 (deltaM-mu ∙ deltaM-mu) (deltaM (mono x)) ∎ |
76 deltaM-association-law functorM monadM (deltaM (delta x d)) = {!!} | 99 deltaM-association-law functorM monadM (deltaM (delta x d)) = {!!} |
77 -} | 100 -} |
78 | 101 |