Trying redenition Delta with length constraints
author Yasutaka Higa Mon, 26 Jan 2015 23:00:05 +0900 a271f3ff1922 9fe3d0bd1149
comparison
equal 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
13 open Functor 14 open Functor
14 open NaturalTransformation 15 open NaturalTransformation
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) ->
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)))}
37
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)
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)))) ⟩
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
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)
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)
89 Monad {l} (\A -> DeltaM M {functorM} {monadM} A n) deltaM-is-functor
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'}