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} ->