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

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
comparison
equal deleted inserted replaced
103:a271f3ff1922 104:ebd0d6e2772c
5 open import basic 5 open import basic
6 open import delta 6 open import delta
7 open import delta.functor 7 open import delta.functor
8 open import deltaM 8 open import deltaM
9 open import deltaM.functor 9 open import deltaM.functor
10 open import nat
10 open import laws 11 open import laws
11 12
12 module deltaM.monad where 13 module deltaM.monad where
13 open Functor 14 open Functor
14 open NaturalTransformation 15 open NaturalTransformation
15 open Monad 16 open Monad
16 17
17 18
18 postulate deltaM-mu-is-natural-transformation : {l : Level} {A : Set l} 19 headDeltaM-commute : {l : Level} {A B : Set l} {n : Nat}
19 {M : {l' : Level} -> Set l' -> Set l'} ->
20 {functorM : {l' : Level} -> Functor {l'} M}
21 {monadM : {l' : Level} -> Monad {l'} M (functorM ) } ->
22 NaturalTransformation (\A -> DeltaM M (DeltaM M A)) (\A -> DeltaM M A)
23 {deltaM-fmap ∙ deltaM-fmap} {deltaM-fmap {l}}
24 (deltaM-mu {_} {_} {M} {functorM} {monadM})
25
26 headDeltaM-commute : {l : Level} {A B : Set l}
27 {M : {l' : Level} -> Set l' -> Set l'} -> 20 {M : {l' : Level} -> Set l' -> Set l'} ->
28 {functorM : {l' : Level} -> Functor {l'} M} -> 21 {functorM : {l' : Level} -> Functor {l'} M} ->
29 {monadM : {l' : Level} -> Monad {l'} M (functorM ) } -> 22 {monadM : {l' : Level} -> Monad {l'} M (functorM ) } ->
30 (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A) -> 23 (f : A -> B) -> (x : DeltaM M {functorM} {monadM} A n) ->
31 headDeltaM (deltaM-fmap f x) ≡ fmap functorM f (headDeltaM x) 24 headDeltaM (deltaM-fmap f x) ≡ fmap functorM f (headDeltaM x)
32 headDeltaM-commute f (deltaM (mono x)) = refl 25 headDeltaM-commute f (deltaM (mono x)) = refl
33 headDeltaM-commute f (deltaM (delta x d)) = refl 26 headDeltaM-commute f (deltaM (delta x d)) = refl
34 27
35 28
36 headDeltaM-is-natural-transformation : {l : Level} {A : Set l} 29 {-
37 {M : {l' : Level} -> Set l' -> Set l'} -> 30 headDeltaM-is-natural-transformation : {l : Level} {A : Set l} {n : Nat}
38 {functorM : {l' : Level} -> Functor {l'} M} 31 {M : {l' : Level} -> Set l' -> Set l'} ->
39 {monadM : {l' : Level} -> Monad {l'} M functorM } -> 32 {functorM : {l' : Level} -> Functor {l'} M}
40 NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A) M 33 {monadM : {l' : Level} -> Monad {l'} M functorM } ->
41 {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))} {fmap functorM} headDeltaM 34 NaturalTransformation {l} (\A -> DeltaM M {functorM} {monadM} A n) M
42 -- {deltaM-fmap} {fmap (functorM {l} {A})} headDeltaM 35 {\f d → deltaM (mono (headDeltaM (deltaM-fmap f d)))}
36 {fmap functorM} headDeltaM
37
43 headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute } 38 headDeltaM-is-natural-transformation = record { commute = headDeltaM-commute }
39 -}
44 40
45 41
46 deltaM-right-unity-law : {l : Level} {A : Set l} 42 deltaM-right-unity-law : {l : Level} {A : Set l}
47 {M : {l' : Level} -> Set l' -> Set l'} 43 {M : {l' : Level} -> Set l' -> Set l'}
48 (functorM : {l' : Level} -> Functor {l'} M) 44 (functorM : {l' : Level} -> Functor {l'} M)
49 (monadM : {l' : Level} -> Monad {l'} M functorM) 45 (monadM : {l' : Level} -> Monad {l'} M functorM)
50 (d : DeltaM M {functorM} {monadM} A) -> 46 (d : DeltaM M {functorM} {monadM} A (S O)) ->
51 (deltaM-mu ∙ deltaM-eta) d ≡ id d 47 (deltaM-mu ∙ deltaM-eta) d ≡ id d
52 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (mono x)) = begin 48 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (mono x)) = begin
53 (deltaM-mu ∙ deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ 49 (deltaM-mu ∙ deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩
54 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ 50 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
55 deltaM-mu (deltaM (mono (eta monadM (deltaM (mono x))))) ≡⟨ refl ⟩ 51 deltaM-mu (deltaM (mono (eta monadM (deltaM (mono x))))) ≡⟨ refl ⟩
56 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x)))))) ≡⟨ refl ⟩ 52 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {S O} {M}) (eta monadM (deltaM (mono x))))))
57 deltaM (mono (mu monadM (fmap functorM (headDeltaM {l} {A} {M}) (eta monadM (deltaM (mono x)))))) 53 ≡⟨ 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)))) ⟩ 54 deltaM (mono (mu monadM (eta monadM (headDeltaM {l} {A} {S O} {M} {functorM} {monadM} (deltaM (mono x))))))
59 deltaM (mono (mu monadM (eta monadM (headDeltaM {l} {A} {M} {functorM} {monadM} (deltaM (mono x)))))) 55 ≡⟨ refl ⟩
60 ≡⟨ refl ⟩ 56 deltaM (mono (mu monadM (eta monadM x)))
61 deltaM (mono (mu monadM (eta {l} monadM x))) 57 ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law monadM x ) )⟩
62 ≡⟨ cong (\x -> deltaM (mono x)) (sym (right-unity-law monadM x)) ⟩
63 deltaM (mono x) 58 deltaM (mono x)
64 ≡⟨ refl ⟩ 59 ≡⟨ refl ⟩
65 id (deltaM (mono x)) 60 id (deltaM (mono x))
66 61
67 deltaM-right-unity-law {l} {A} {M} functorM monadM (deltaM (delta x d)) = begin 62 deltaM-right-unity-law functorM monadM (deltaM (delta x ()))
68 (deltaM-mu ∙ deltaM-eta) (deltaM (delta x d)) ≡⟨ refl ⟩ 63 -- cannot apply (mu ∙ eta) for over 2 version delta.
69 deltaM-mu (deltaM-eta (deltaM (delta x d))) ≡⟨ refl ⟩ 64
70 deltaM-mu (deltaM (mono (eta monadM (deltaM (delta x d))))) ≡⟨ refl ⟩ 65
71 deltaM (mono (mu monadM (fmap functorM headDeltaM (eta monadM (deltaM (delta x d)))))) 66 {-
72 ≡⟨ cong (\de -> deltaM (mono (mu monadM de))) (sym (eta-is-nt monadM headDeltaM (deltaM (delta x d)))) ⟩ 67 deltaM-left-unity-law : {l : Level} {A : Set l}
73 deltaM (mono (mu monadM (eta monadM (headDeltaM (deltaM (delta x d)))))) 68 {M : {l' : Level} -> Set l' -> Set l'}
74 ≡⟨ refl ⟩ 69 (functorM : {l' : Level} -> Functor {l'} M)
75 deltaM (mono (mu monadM (eta monadM x))) 70 (monadM : {l' : Level} -> Monad {l'} M functorM)
76 ≡⟨ {!!} ⟩ 71 (d : DeltaM M {functorM} {monadM} A (S O)) ->
77 id (deltaM (delta x d)) 72 (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d
78 73 deltaM-left-unity-law functorM monadM (deltaM (mono x)) = begin
74 (deltaM-mu ∙ deltaM-fmap deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩
75 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
76 deltaM-mu (deltaM (mono (fmap functorM deltaM-eta x))) ≡⟨ refl ⟩
77 deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩
78 deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩
79
80 id (deltaM (mono x))
81
82 deltaM-left-unity-law functorM monadM (deltaM (delta x ()))
83 -}
84
85 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
86 {M : {l' : Level} -> Set l' -> Set l'}
87 (functorM : {l' : Level} -> Functor {l'} M)
88 (monadM : {l' : Level}-> Monad {l'} M functorM) ->
89 Monad {l} (\A -> DeltaM M {functorM} {monadM} A n) deltaM-is-functor
90 deltaM-is-monad functorM monadM = record
91 { mu = deltaM-mu;
92 eta = deltaM-eta;
93 return = {!!};
94 bind = {!!};
95 association-law = {!!};
96 left-unity-law = {!!};
97 right-unity-law = {!!};
98 eta-is-nt = {!!}
99 }
100
101
102
103
79 104
80 105
81 {- 106 {-
82 deltaM-association-law : {l : Level} {A : Set l} 107 deltaM-association-law : {l : Level} {A : Set l}
83 {M : {l' : Level} -> Set l' -> Set l'} 108 {M : {l' : Level} -> Set l' -> Set l'}