Mercurial > hg > Members > atton > delta_monad
comparison agda/deltaM/functor.agda @ 92:4d615910c87a
Prove preserve-id for deltaM
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 19 Jan 2015 14:32:07 +0900 |
parents | f41682b53992 |
children | 8d92ed54a94f |
comparison
equal
deleted
inserted
replaced
91:f41682b53992 | 92:4d615910c87a |
---|---|
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) ⟩ |
24 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩ | 24 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩ |
25 deltaM (mono x) ∎ | 25 deltaM (mono x) ∎ |
26 deltaM-preserve-id functorM (deltaM (delta x d)) = begin | 26 deltaM-preserve-id functorM (deltaM (delta x d)) = begin |
27 deltaM-fmap id (deltaM (delta x d)) ≡⟨ refl ⟩ | 27 deltaM-fmap id (deltaM (delta x d)) |
28 deltaM (fmap delta-is-functor (fmap functorM id) (delta x d)) ≡⟨ {!!} ⟩ | 28 ≡⟨ refl ⟩ |
29 deltaM (fmap delta-is-functor (fmap functorM id) (delta x d)) | |
30 ≡⟨ refl ⟩ | |
31 deltaM (delta (fmap functorM id x) (fmap delta-is-functor (fmap functorM id) d)) | |
32 ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))) (preserve-id functorM x) ⟩ | |
33 deltaM (delta x (fmap delta-is-functor (fmap functorM id) d)) | |
34 ≡⟨ refl ⟩ | |
35 appendDeltaM (deltaM (mono x)) (deltaM (fmap delta-is-functor (fmap functorM id) d)) | |
36 ≡⟨ refl ⟩ | |
37 appendDeltaM (deltaM (mono x)) (deltaM-fmap id (deltaM d)) | |
38 ≡⟨ cong (\d -> appendDeltaM (deltaM (mono x)) d) (deltaM-preserve-id functorM (deltaM d)) ⟩ | |
39 appendDeltaM (deltaM (mono x)) (deltaM d) | |
40 ≡⟨ refl ⟩ | |
29 deltaM (delta x d) | 41 deltaM (delta x d) |
30 ∎ | 42 ∎ |
31 | 43 |
32 {- | 44 {- |
33 deltaM-covariant : {l : Level} {A B C : Set l} -> | 45 deltaM-covariant : {l : Level} {A B C : Set l} -> |