Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/functor.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 8d92ed54a94f
children ebd0d6e2772c
comparison
equal deleted inserted replaced
102:9c62373bd474 103:a271f3ff1922
13 13
14 14
15 deltaM-preserve-id : {l : Level} {A : Set l} 15 deltaM-preserve-id : {l : Level} {A : Set l}
16 {M : {l' : Level} -> Set l' -> Set l'} 16 {M : {l' : Level} -> Set l' -> Set l'}
17 (functorM : {l' : Level} -> Functor {l'} M) 17 (functorM : {l' : Level} -> Functor {l'} M)
18 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 18 {monadM : {l' : Level} -> Monad {l'} M functorM}
19 -> (d : DeltaM M {functorM} {monadM} A) -> deltaM-fmap id d ≡ id d 19 -> (d : DeltaM M {functorM} {monadM} A) -> deltaM-fmap id d ≡ id d
20 deltaM-preserve-id functorM (deltaM (mono x)) = begin 20 deltaM-preserve-id functorM (deltaM (mono x)) = begin
21 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩ 21 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩
22 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩ 22 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩
23 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩ 23 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩
43 43
44 44
45 deltaM-covariant : {l : Level} {A B C : Set l} -> 45 deltaM-covariant : {l : Level} {A B C : Set l} ->
46 {M : {l' : Level} -> Set l' -> Set l'} 46 {M : {l' : Level} -> Set l' -> Set l'}
47 (functorM : {l' : Level} -> Functor {l'} M) 47 (functorM : {l' : Level} -> Functor {l'} M)
48 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 48 {monadM : {l' : Level} -> Monad {l'} M functorM}
49 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A) -> 49 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A) ->
50 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d 50 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d
51 deltaM-covariant functorM f g (deltaM (mono x)) = begin 51 deltaM-covariant functorM f g (deltaM (mono x)) = begin
52 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩ 52 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩
53 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩ 53 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩
79 ∎ 79 ∎
80 80
81 81
82 deltaM-is-functor : {l : Level} {M : {l' : Level} -> Set l' -> Set l'} 82 deltaM-is-functor : {l : Level} {M : {l' : Level} -> Set l' -> Set l'}
83 {functorM : {l' : Level} -> Functor {l'} M } 83 {functorM : {l' : Level} -> Functor {l'} M }
84 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 84 {monadM : {l' : Level} -> Monad {l'} M functorM}
85 -> Functor {l} (DeltaM M {functorM} {monadM}) 85 -> Functor {l} (DeltaM M {functorM} {monadM})
86 deltaM-is-functor {_} {_} {functorM} = record { fmap = deltaM-fmap ; 86 deltaM-is-functor {_} {_} {functorM} = record { fmap = deltaM-fmap ;
87 preserve-id = deltaM-preserve-id functorM ; 87 preserve-id = deltaM-preserve-id functorM ;
88 covariant = (\f g -> deltaM-covariant functorM g f)} 88 covariant = (\f g -> deltaM-covariant functorM g f)}