Mercurial > hg > Members > kono > Proof > category
annotate nat.agda @ 26:ad62c87659ef
join association finish
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 12 Jul 2013 20:45:54 +0900 |
parents | 8117bafdec7a |
children | d9c2386a18a8 |
rev | line source |
---|---|
0 | 1 module nat where |
2 | |
3 -- Monad | |
4 -- Category A | |
5 -- A = Category | |
22 | 6 -- Functor T : A → A |
0 | 7 --T(a) = t(a) |
8 --T(f) = tf(f) | |
9 | |
2 | 10 open import Category -- https://github.com/konn/category-agda |
0 | 11 open import Level |
12 open Functor | |
13 | |
1 | 14 --T(g f) = T(g) T(f) |
15 | |
22 | 16 Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b } |
17 → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] | |
18 Lemma1 = \t → IsFunctor.distr ( isFunctor t ) | |
0 | 19 |
20 -- F(f) | |
22 | 21 -- F(a) ---→ F(b) |
0 | 22 -- | | |
23 -- |t(a) |t(b) G(f)t(a) = t(b)F(f) | |
24 -- | | | |
25 -- v v | |
22 | 26 -- G(a) ---→ G(b) |
0 | 27 -- G(f) |
28 | |
7 | 29 record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) |
0 | 30 ( F G : Functor D C ) |
7 | 31 (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A)) |
0 | 32 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where |
33 field | |
34 naturality : {a b : Obj D} {f : Hom D a b} | |
7 | 35 → C [ C [ ( FMap G f ) o ( Trans a ) ] ≈ C [ (Trans b ) o (FMap F f) ] ] |
0 | 36 -- uniqness : {d : Obj D} |
7 | 37 -- → C [ Trans d ≈ Trans d ] |
0 | 38 |
39 | |
7 | 40 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain ) |
0 | 41 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where |
42 field | |
7 | 43 Trans : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) |
44 isNTrans : IsNTrans domain codomain F G Trans | |
0 | 45 |
7 | 46 open NTrans |
1 | 47 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} |
22 | 48 → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b } |
49 → A [ A [ FMap G f o Trans μ a ] ≈ A [ Trans μ b o FMap F f ] ] | |
50 Lemma2 = \n → IsNTrans.naturality ( isNTrans n ) | |
0 | 51 |
52 open import Category.Cat | |
53 | |
22 | 54 -- η : 1_A → T |
55 -- μ : TT → T | |
0 | 56 -- μ(a)η(T(a)) = a |
57 -- μ(a)T(η(a)) = a | |
58 -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) | |
59 | |
1 | 60 record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
61 ( T : Functor A A ) | |
7 | 62 ( η : NTrans A A identityFunctor T ) |
63 ( μ : NTrans A A (T ○ T) T) | |
1 | 64 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
65 field | |
22 | 66 assoc : {a : Obj A} → A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] |
67 unity1 : {a : Obj A} → A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
68 unity2 : {a : Obj A} → A [ A [ Trans μ a o (FMap T (Trans η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] | |
0 | 69 |
7 | 70 record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) |
1 | 71 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
7 | 72 eta : NTrans A A identityFunctor T |
6 | 73 eta = η |
7 | 74 mu : NTrans A A (T ○ T) T |
6 | 75 mu = μ |
1 | 76 field |
77 isMonad : IsMonad A T η μ | |
0 | 78 |
2 | 79 open Monad |
80 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
81 { T : Functor A A } | |
7 | 82 { η : NTrans A A identityFunctor T } |
83 { μ : NTrans A A (T ○ T) T } | |
22 | 84 { a : Obj A } → |
2 | 85 ( M : Monad A T η μ ) |
22 | 86 → A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] |
87 Lemma3 = \m → IsMonad.assoc ( isMonad m ) | |
2 | 88 |
89 | |
90 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b} | |
22 | 91 → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ] |
92 Lemma4 = \a → IsCategory.identityL ( Category.isCategory a ) | |
0 | 93 |
3 | 94 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} |
95 { T : Functor A A } | |
7 | 96 { η : NTrans A A identityFunctor T } |
97 { μ : NTrans A A (T ○ T) T } | |
22 | 98 { a : Obj A } → |
3 | 99 ( M : Monad A T η μ ) |
22 | 100 → A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
101 Lemma5 = \m → IsMonad.unity1 ( isMonad m ) | |
3 | 102 |
103 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} | |
104 { T : Functor A A } | |
7 | 105 { η : NTrans A A identityFunctor T } |
106 { μ : NTrans A A (T ○ T) T } | |
22 | 107 { a : Obj A } → |
3 | 108 ( M : Monad A T η μ ) |
22 | 109 → A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] |
110 Lemma6 = \m → IsMonad.unity2 ( isMonad m ) | |
3 | 111 |
112 -- T = M x A | |
0 | 113 -- nat of η |
114 -- g ○ f = μ(c) T(g) f | |
115 -- η(b) ○ f = f | |
116 -- f ○ η(a) = f | |
22 | 117 -- h ○ (g ○ f) = (h ○ g) ○ f |
0 | 118 |
4 | 119 record Kleisli { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) |
120 ( T : Functor A A ) | |
7 | 121 ( η : NTrans A A identityFunctor T ) |
122 ( μ : NTrans A A (T ○ T) T ) | |
4 | 123 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
5 | 124 monad : Monad A T η μ |
125 monad = M | |
22 | 126 -- g ○ f = μ(c) T(g) f |
127 join : { a b : Obj A } → ( c : Obj A ) → | |
128 ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) | |
7 | 129 join c g f = A [ Trans μ c o A [ FMap T g o f ] ] |
130 | |
10 | 131 |
7 | 132 |
18 | 133 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where |
22 | 134 open import Relation.Binary.Core renaming ( Trans to Trasn1 ) |
7 | 135 |
18 | 136 refl-hom : {a b : Obj A } { x : Hom A a b } → |
137 A [ x ≈ x ] | |
138 refl-hom = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) | |
8 | 139 |
18 | 140 trans-hom : {a b : Obj A } |
141 { x y z : Hom A a b } → | |
142 A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ] | |
143 trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory A ))) b c | |
5 | 144 |
22 | 145 -- some short cuts |
146 | |
147 car-eq : {a b c : Obj A } {x y : Hom A a b } ( f : Hom A c a ) → | |
148 A [ x ≈ y ] → A [ A [ x o f ] ≈ A [ y o f ] ] | |
149 car-eq f eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq | |
150 | |
151 cdr-eq : {a b c : Obj A } {x y : Hom A a b } ( f : Hom A b c ) → | |
152 A [ x ≈ y ] → A [ A [ f o x ] ≈ A [ f o y ] ] | |
153 cdr-eq f eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) | |
154 | |
155 id : (a : Obj A ) → Hom A a a | |
156 id a = (Id {_} {_} {_} {A} a) | |
157 | |
158 idL : {a b : Obj A } { f : Hom A b a } → A [ A [ id a o f ] ≈ f ] | |
159 idL = IsCategory.identityL (Category.isCategory A) | |
160 | |
161 idR : {a b : Obj A } { f : Hom A a b } → A [ A [ f o id a ] ≈ f ] | |
162 idR = IsCategory.identityR (Category.isCategory A) | |
163 | |
23 | 164 sym : {a b : Obj A } { f g : Hom A a b } -> A [ f ≈ g ] -> A [ g ≈ f ] |
165 sym = IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) | |
166 | |
22 | 167 assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} |
168 → A [ A [ f o A [ g o h ] ] ≈ A [ A [ f o g ] o h ] ] | |
169 assoc = IsCategory.associative (Category.isCategory A) | |
170 | |
24 | 171 distr : (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b } |
22 | 172 → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] |
24 | 173 distr T = IsFunctor.distr ( isFunctor T ) |
22 | 174 |
175 nat : { c₁′ c₂′ ℓ′ : Level} (D : Category c₁′ c₂′ ℓ′) {a b : Obj D} {f : Hom D a b} {F G : Functor D A } | |
176 → (η : NTrans D A F G ) | |
177 → A [ A [ ( FMap G f ) o ( Trans η a ) ] ≈ A [ (Trans η b ) o (FMap F f) ] ] | |
178 nat _ η = IsNTrans.naturality ( isNTrans η ) | |
179 | |
18 | 180 infixr 2 _∎ |
181 infixr 2 _≈⟨_⟩_ | |
182 infix 1 begin_ | |
7 | 183 |
12 | 184 |
18 | 185 data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) : |
186 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
187 relTo : (x≈y : A [ x ≈ y ] ) → x IsRelatedTo y | |
17 | 188 |
18 | 189 begin_ : { a b : Obj A } { x y : Hom A a b } → |
190 x IsRelatedTo y → A [ x ≈ y ] | |
191 begin relTo x≈y = x≈y | |
17 | 192 |
18 | 193 _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → |
194 A [ x ≈ y ] → y IsRelatedTo z → x IsRelatedTo z | |
195 _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z) | |
17 | 196 |
18 | 197 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x |
198 _∎ _ = relTo refl-hom | |
17 | 199 |
22 | 200 lemma12 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } → |
201 ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ] | |
18 | 202 lemma12 L x y = |
203 let open ≈-Reasoning ( L ) in | |
204 begin L [ x o y ] ∎ | |
11 | 205 |
22 | 206 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → |
207 { a : Obj A } ( b : Obj A ) → | |
17 | 208 ( f : Hom A a b ) |
22 | 209 → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ f ] |
18 | 210 Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) |
211 let open ≈-Reasoning (c) in | |
17 | 212 begin |
18 | 213 c [ Id {_} {_} {_} {c} b o g ] |
214 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ | |
17 | 215 g |
216 ∎ | |
11 | 217 |
4 | 218 open Kleisli |
22 | 219 -- η(b) ○ f = f |
220 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → | |
21 | 221 ( T : Functor A A ) |
222 ( η : NTrans A A identityFunctor T ) | |
7 | 223 { μ : NTrans A A (T ○ T) T } |
21 | 224 { a : Obj A } ( b : Obj A ) |
225 ( f : Hom A a ( FObj T b) ) | |
22 | 226 ( m : Monad A T η μ ) |
227 ( k : Kleisli A T η μ m) | |
228 → A [ join k b (Trans η b) f ≈ f ] | |
21 | 229 Lemma7 c T η b f m k = |
230 let open ≈-Reasoning (c) | |
231 μ = mu ( monad k ) | |
232 in | |
233 begin | |
234 join k b (Trans η b) f | |
235 ≈⟨ refl-hom ⟩ | |
236 c [ Trans μ b o c [ FMap T ((Trans η b)) o f ] ] | |
237 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ | |
238 c [ c [ Trans μ b o FMap T ((Trans η b)) ] o f ] | |
22 | 239 ≈⟨ car-eq f ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ |
240 c [ id (FObj T b) o f ] | |
21 | 241 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ |
242 f | |
243 ∎ | |
7 | 244 |
22 | 245 -- f ○ η(a) = f |
246 Lemma8 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) | |
247 ( T : Functor A A ) | |
248 ( η : NTrans A A identityFunctor T ) | |
7 | 249 { μ : NTrans A A (T ○ T) T } |
22 | 250 ( a : Obj A ) ( b : Obj A ) |
251 ( f : Hom A a ( FObj T b) ) | |
252 ( m : Monad A T η μ ) | |
253 ( k : Kleisli A T η μ m) | |
254 → A [ join k b f (Trans η a) ≈ f ] | |
255 Lemma8 c T η a b f m k = | |
256 begin | |
257 join k b f (Trans η a) | |
258 ≈⟨ refl-hom ⟩ | |
259 c [ Trans μ b o c [ FMap T f o (Trans η a) ] ] | |
260 ≈⟨ cdr-eq (Trans μ b) ( IsNTrans.naturality ( isNTrans η )) ⟩ | |
261 c [ Trans μ b o c [ (Trans η ( FObj T b)) o f ] ] | |
262 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ | |
263 c [ c [ Trans μ b o (Trans η ( FObj T b)) ] o f ] | |
264 ≈⟨ car-eq f ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩ | |
265 c [ id (FObj T b) o f ] | |
266 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ | |
267 f | |
268 ∎ where | |
269 open ≈-Reasoning (c) | |
270 μ = mu ( monad k ) | |
5 | 271 |
22 | 272 -- h ○ (g ○ f) = (h ○ g) ○ f |
23 | 273 Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
274 ( T : Functor A A ) | |
275 ( η : NTrans A A identityFunctor T ) | |
276 ( μ : NTrans A A (T ○ T) T ) | |
277 ( a b c d : Obj A ) | |
278 ( f : Hom A a ( FObj T b) ) | |
279 ( g : Hom A b ( FObj T c) ) | |
280 ( h : Hom A c ( FObj T d) ) | |
281 ( m : Monad A T η μ ) | |
282 ( k : Kleisli A T η μ m) | |
22 | 283 → A [ join k d h (join k c g f) ≈ join k d ( join k d h g) f ] |
24 | 284 Lemma9 A T η μ a b c d f g h m k = |
285 begin | |
23 | 286 join k d h (join k c g f) |
287 ≈⟨ refl-hom ⟩ | |
288 join k d h ( A [ Trans μ c o A [ FMap T g o f ] ] ) | |
289 ≈⟨ refl-hom ⟩ | |
290 A [ Trans μ d o A [ FMap T h o A [ Trans μ c o A [ FMap T g o f ] ] ] ] | |
25 | 291 ≈⟨ cdr-eq ( Trans μ d ) ( cdr-eq ( FMap T h ) ( assoc )) ⟩ |
292 A [ Trans μ d o A [ FMap T h o A [ A [ Trans μ c o FMap T g ] o f ] ] ] | |
293 ≈⟨ assoc ⟩ --- A [ f x A [ g x h ] ] = A [ A [ f x g ] x h ] | |
294 A [ A [ Trans μ d o FMap T h ] o A [ A [ Trans μ c o FMap T g ] o f ] ] | |
295 ≈⟨ assoc ⟩ | |
296 A [ A [ A [ Trans μ d o FMap T h ] o A [ Trans μ c o FMap T g ] ] o f ] | |
297 ≈⟨ car-eq f (sym assoc) ⟩ | |
298 A [ A [ Trans μ d o A [ FMap T h o A [ Trans μ c o FMap T g ] ] ] o f ] | |
299 ≈⟨ car-eq f ( cdr-eq ( Trans μ d ) (assoc) ) ⟩ | |
300 A [ A [ Trans μ d o A [ A [ FMap T h o Trans μ c ] o FMap T g ] ] o f ] | |
301 ≈⟨ car-eq f assoc ⟩ | |
302 A [ A [ A [ Trans μ d o A [ FMap T h o Trans μ c ] ] o FMap T g ] o f ] | |
303 ≈⟨ car-eq f (car-eq ( FMap T g) ( cdr-eq ( Trans μ d ) ( begin | |
26
ad62c87659ef
join association finish
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
25
diff
changeset
|
304 A [ FMap T h o Trans μ c ] |
ad62c87659ef
join association finish
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
25
diff
changeset
|
305 ≈⟨ nat A μ ⟩ |
ad62c87659ef
join association finish
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
25
diff
changeset
|
306 A [ Trans μ (FObj T d) o FMap T (FMap T h) ] |
25 | 307 ∎ |
308 ))) ⟩ | |
309 A [ A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o FMap T ( FMap T h ) ] ] o FMap T g ] o f ] | |
26
ad62c87659ef
join association finish
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
25
diff
changeset
|
310 ≈⟨ car-eq f (sym assoc) ⟩ |
25 | 311 A [ A [ Trans μ d o A [ A [ Trans μ ( FObj T d) o FMap T ( FMap T h ) ] o FMap T g ] ] o f ] |
312 ≈⟨ car-eq f ( cdr-eq ( Trans μ d ) (sym assoc) ) ⟩ | |
313 A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o A [ FMap T ( FMap T h ) o FMap T g ] ] ] o f ] | |
314 ≈⟨ car-eq f ( cdr-eq ( Trans μ d) (cdr-eq (Trans μ ( FObj T d) ) (sym (distr T )))) ⟩ | |
315 A [ A [ Trans μ d o A [ Trans μ ( FObj T d) o FMap T ( A [ FMap T h o g ] ) ] ] o f ] | |
316 ≈⟨ car-eq f assoc ⟩ | |
24 | 317 A [ A [ A [ Trans μ d o Trans μ ( FObj T d) ] o FMap T ( A [ FMap T h o g ] ) ] o f ] |
25 | 318 ≈⟨ car-eq f ( car-eq (FMap T ( A [ FMap T h o g ] )) ( IsMonad.assoc ( isMonad m ))) ⟩ |
24 | 319 A [ A [ A [ Trans μ d o FMap T ( Trans μ d) ] o FMap T ( A [ FMap T h o g ] ) ] o f ] |
320 ≈⟨ car-eq f (sym assoc) ⟩ | |
321 A [ A [ Trans μ d o A [ FMap T ( Trans μ d ) o FMap T ( A [ FMap T h o g ] ) ] ] o f ] | |
322 ≈⟨ sym assoc ⟩ | |
23 | 323 A [ Trans μ d o A [ A [ FMap T ( Trans μ d ) o FMap T ( A [ FMap T h o g ] ) ] o f ] ] |
24 | 324 ≈⟨ cdr-eq ( Trans μ d ) ( car-eq f ( sym ( distr T ))) ⟩ |
23 | 325 A [ Trans μ d o A [ FMap T ( A [ ( Trans μ d ) o A [ FMap T h o g ] ] ) o f ] ] |
326 ≈⟨ refl-hom ⟩ | |
327 join k d ( A [ Trans μ d o A [ FMap T h o g ] ] ) f | |
328 ≈⟨ refl-hom ⟩ | |
329 join k d ( join k d h g) f | |
24 | 330 ∎ where open ≈-Reasoning (A) |
3 | 331 |
332 | |
333 | |
334 -- Kleisli : | |
335 -- Kleisli = record { Hom = | |
336 -- ; Hom = _⟶_ | |
337 -- ; Id = IdProd | |
338 -- ; _o_ = _∘_ | |
339 -- ; _≈_ = _≈_ | |
340 -- ; isCategory = record { isEquivalence = record { refl = λ {φ} → ≈-refl {φ = φ} | |
341 -- ; sym = λ {φ ψ} → ≈-symm {φ = φ} {ψ} | |
342 -- ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ} | |
343 -- } | |
344 -- ; identityL = identityL | |
345 -- ; identityR = identityR | |
346 -- ; o-resp-≈ = o-resp-≈ | |
347 -- ; associative = associative | |
348 -- } | |
349 -- } |