Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/functor.agda @ 112:0a3b6cb91a05

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove left-unity-law for DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 30 Jan 2015 21:57:31 +0900
parents cd058dd89864
children 47f144540d51
comparison
equal deleted inserted replaced
111:9fe3d0bd1149 112:0a3b6cb91a05
12 12
13 module deltaM.functor where 13 module deltaM.functor where
14 14
15 15
16 deltaM-preserve-id : {l : Level} {A : Set l} {n : Nat} 16 deltaM-preserve-id : {l : Level} {A : Set l} {n : Nat}
17 {M : {l' : Level} -> Set l' -> Set l'} 17 {M : Set l -> Set l}
18 (functorM : {l' : Level} -> Functor {l'} M) 18 (functorM : Functor M)
19 {monadM : {l' : Level} -> Monad {l'} M functorM} 19 {monadM : Monad M functorM}
20 -> (d : DeltaM M {functorM} {monadM} A (S n)) -> deltaM-fmap id d ≡ id d 20 -> (d : DeltaM M {functorM} {monadM} A (S n)) -> deltaM-fmap id d ≡ id d
21 deltaM-preserve-id functorM (deltaM (mono x)) = begin 21 deltaM-preserve-id functorM (deltaM (mono x)) = begin
22 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩ 22 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩
23 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩ 23 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩
24 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩ 24 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩
42 deltaM (delta x d) 42 deltaM (delta x d)
43 ∎ 43 ∎
44 44
45 45
46 deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat} -> 46 deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat} ->
47 {M : {l' : Level} -> Set l' -> Set l'} 47 {M : Set l -> Set l}
48 (functorM : {l' : Level} -> Functor {l'} M) 48 (functorM : Functor M)
49 {monadM : {l' : Level} -> Monad {l'} M functorM} 49 {monadM : Monad M functorM}
50 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A (S n)) -> 50 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A (S n)) ->
51 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d 51 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d
52 deltaM-covariant functorM f g (deltaM (mono x)) = begin 52 deltaM-covariant functorM f g (deltaM (mono x)) = begin
53 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩ 53 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩
54 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩ 54 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩
77 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d)) 77 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d))
78 ≡⟨ refl ⟩ 78 ≡⟨ refl ⟩
79 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d)) 79 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
80 ∎ 80 ∎
81 81
82 postulate deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat}
83 {M : Set l -> Set l}
84 {functorM : Functor M}
85 {monadM : Monad M functorM}
86 {f g : A -> B}
87 (eq : (x : A) -> f x ≡ g x)
88 (d : DeltaM M {functorM} {monadM} A (S n)) ->
89 deltaM-fmap f d ≡ deltaM-fmap g d
90 {-
91 deltaM-fmap-equiv {n = O} f g eq (deltaM (mono x)) = begin
92 {!!} ≡⟨ {!!} ⟩
93 {!!}
94 ∎
95 deltaM-fmap-equiv {n = S n} f g eq d = {!!}
96 -}
82 97
83 deltaM-is-functor : {l : Level} {n : Nat} 98 deltaM-is-functor : {l : Level} {n : Nat}
84 {M : {l' : Level} -> Set l' -> Set l'} 99 {M : Set l -> Set l}
85 {functorM : {l' : Level} -> Functor {l'} M } 100 {functorM : Functor M }
86 {monadM : {l' : Level} -> Monad {l'} M functorM} 101 {monadM : Monad M functorM}
87 -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) 102 -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A (S n))
88 deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ; 103 deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ;
89 preserve-id = deltaM-preserve-id functorM ; 104 preserve-id = deltaM-preserve-id functorM ;
90 covariant = (\f g -> deltaM-covariant functorM g f)} 105 covariant = (\f g -> deltaM-covariant functorM g f);
106 fmap-equiv = deltaM-fmap-equiv
107 }