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

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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open ≡-Reasoning
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import basic
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import delta
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import delta.functor
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import deltaM
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
9 open import nat
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import laws
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open Functor
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 module deltaM.functor where
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
16 deltaM-preserve-id : {l : Level} {A : Set l} {n : Nat}
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
17 {M : Set l -> Set l}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
18 (functorM : Functor M)
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
19 {monadM : Monad M functorM}
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
20 -> (d : DeltaM M {functorM} {monadM} A (S n)) -> deltaM-fmap id d ≡ id d
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 deltaM-preserve-id functorM (deltaM (mono x)) = begin
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 deltaM (fmap delta-is-functor (fmap functorM id) (mono x)) ≡⟨ refl ⟩
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
24 deltaM (mono (fmap functorM id x)) ≡⟨ cong (\x -> deltaM (mono x)) (preserve-id functorM x) ⟩
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 deltaM (mono (id x)) ≡⟨ cong (\x -> deltaM (mono x)) refl ⟩
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 deltaM (mono x) ∎
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 deltaM-preserve-id functorM (deltaM (delta x d)) = begin
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
28 deltaM-fmap id (deltaM (delta x d))
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
29 ≡⟨ refl ⟩
92
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
30 deltaM (fmap delta-is-functor (fmap functorM id) (delta x d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
31 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
32 deltaM (delta (fmap functorM id x) (fmap delta-is-functor (fmap functorM id) d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
33 ≡⟨ cong (\x -> deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))) (preserve-id functorM x) ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
34 deltaM (delta x (fmap delta-is-functor (fmap functorM id) d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
35 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
36 appendDeltaM (deltaM (mono x)) (deltaM (fmap delta-is-functor (fmap functorM id) d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
37 ≡⟨ refl ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
38 appendDeltaM (deltaM (mono x)) (deltaM-fmap id (deltaM d))
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
39 ≡⟨ cong (\d -> appendDeltaM (deltaM (mono x)) d) (deltaM-preserve-id functorM (deltaM d)) ⟩
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
40 appendDeltaM (deltaM (mono x)) (deltaM d)
4d615910c87a Prove preserve-id for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
41 ≡⟨ refl ⟩
91
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 deltaM (delta x d)
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
f41682b53992 Prove deltaM-preserve-id by mono
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
45
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
46 deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat} ->
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
47 {M : Set l -> Set l}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
48 (functorM : Functor M)
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
49 {monadM : Monad M functorM}
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
50 (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A (S n)) ->
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
51 (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
52 deltaM-covariant functorM f g (deltaM (mono x)) = begin
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
53 deltaM-fmap (f ∙ g) (deltaM (mono x)) ≡⟨ refl ⟩
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
54 deltaM (delta-fmap (fmap functorM (f ∙ g)) (mono x)) ≡⟨ refl ⟩
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
55 deltaM (mono (fmap functorM (f ∙ g) x)) ≡⟨ cong (\x -> (deltaM (mono x))) (covariant functorM g f x) ⟩
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
56 deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x)) ≡⟨ refl ⟩
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
57 deltaM-fmap f (deltaM-fmap g (deltaM (mono x))) ∎
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
58 deltaM-covariant functorM f g (deltaM (delta x d)) = begin
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
59 deltaM-fmap (f ∙ g) (deltaM (delta x d))
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
60 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
61 deltaM (delta-fmap (fmap functorM (f ∙ g)) (delta x d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
62 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
63 deltaM (delta (fmap functorM (f ∙ g) x) (delta-fmap (fmap functorM (f ∙ g)) d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
64 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
65 appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM (delta-fmap (fmap functorM (f ∙ g)) d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
66 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
67 appendDeltaM (deltaM (mono (fmap functorM (f ∙ g) x))) (deltaM-fmap (f ∙ g) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
68 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-fmap (f ∙ g) (deltaM d))) (covariant functorM g f x) ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
69 appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
70 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
71 appendDeltaM (deltaM (mono (((fmap functorM f) ∙ (fmap functorM g)) x))) (deltaM-fmap (f ∙ g) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
72 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
73 appendDeltaM (deltaM (delta-fmap ((fmap functorM f) ∙ (fmap functorM g)) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
74 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
75 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (deltaM-fmap (f ∙ g) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
76 ≡⟨ cong (\de -> appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) de) (deltaM-covariant functorM f g (deltaM d)) ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
77 appendDeltaM (deltaM ((((delta-fmap (fmap functorM f)) ∙ (delta-fmap (fmap functorM g)))) (mono x))) (((deltaM-fmap f) ∙ (deltaM-fmap g)) (deltaM d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
78 ≡⟨ refl ⟩
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
79 (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d))
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
80
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
81
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
82 postulate deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
83 {M : Set l -> Set l}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
84 {functorM : Functor M}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
85 {monadM : Monad M functorM}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
86 {f g : A -> B}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
87 (eq : (x : A) -> f x ≡ g x)
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
88 (d : DeltaM M {functorM} {monadM} A (S n)) ->
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
89 deltaM-fmap f d ≡ deltaM-fmap g d
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
90 {-
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
91 deltaM-fmap-equiv {n = O} f g eq (deltaM (mono x)) = begin
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
92 {!!} ≡⟨ {!!} ⟩
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
93 {!!}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
94
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
95 deltaM-fmap-equiv {n = S n} f g eq d = {!!}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
96 -}
93
8d92ed54a94f Prove functor-laws for deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 92
diff changeset
97
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
98 deltaM-is-functor : {l : Level} {n : Nat}
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
99 {M : Set l -> Set l}
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
100 {functorM : Functor M }
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
101 {monadM : Monad M functorM}
110
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
102 -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A (S n))
cd058dd89864 Rewrite Functor-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
103 deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ;
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
104 preserve-id = deltaM-preserve-id functorM ;
112
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
105 covariant = (\f g -> deltaM-covariant functorM g f);
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
106 fmap-equiv = deltaM-fmap-equiv
0a3b6cb91a05 Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 110
diff changeset
107 }