Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/functor.agda @ 91:f41682b53992

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove deltaM-preserve-id by mono
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 12:29:29 +0900
parents
children 4d615910c87a
comparison
equal deleted inserted replaced
90:55d11ce7e223 91:f41682b53992
1 open import Level
2 open import Relation.Binary.PropositionalEquality
3 open ≡-Reasoning
4
5 open import basic
6 open import delta
7 open import delta.functor
8 open import deltaM
9 open import laws
10 open Functor
11
12 module deltaM.functor where
13
14
15 deltaM-preserve-id : {l : Level} {A : Set l}
16 {M : {l' : Level} -> Set l' -> Set l'}
17 (functorM : {l' : Level} -> Functor {l'} M)
18 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
19 -> (d : DeltaM M {functorM} {monadM} A) -> (deltaM-fmap id) d ≡ id d
20 deltaM-preserve-id functorM (deltaM (mono x)) = begin
21 deltaM-fmap id (deltaM (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) ⟩
24 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩
25 deltaM (mono x) ∎
26 deltaM-preserve-id functorM (deltaM (delta x d)) = begin
27 deltaM-fmap id (deltaM (delta x d)) ≡⟨ refl ⟩
28 deltaM (fmap delta-is-functor (fmap functorM id) (delta x d)) ≡⟨ {!!} ⟩
29 deltaM (delta x d)
30 ∎
31
32 {-
33 deltaM-covariant : {l : Level} {A B C : Set l} ->
34 (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
35 (delta-fmap (f ∙ g)) d ≡ (delta-fmap f) (delta-fmap g d)
36 deltaM-covariant = {!!}
37 -}