Mercurial > hg > Members > kono > Proof > category

comparison CCChom.agda @ 795:030c5b87ed78

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ccc to adjunction done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Apr 2019 18:00:03 +0900
parents ba575c73ea48
children 82a8c1ab4ef5
comparison
equal deleted inserted replaced
794:ba575c73ea48 795:030c5b87ed78
2 open import Category 2 open import Category
3 module CCChom where 3 module CCChom where
4 4
5 open import HomReasoning 5 open import HomReasoning
6 open import cat-utility 6 open import cat-utility
7 open import Data.Product renaming (_×_ to _∧_) 7 open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> )
8 open import Category.Constructions.Product 8 open import Category.Constructions.Product
9 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
10 10
11 open Functor 11 open Functor
12 12
168 168
169 U_b : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( ccc : CCC A ) → (b : Obj A) → Functor A A 169 U_b : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( ccc : CCC A ) → (b : Obj A) → Functor A A
170 FObj (U_b A ccc b) = λ a → (CCC._<=_ ccc a b ) 170 FObj (U_b A ccc b) = λ a → (CCC._<=_ ccc a b )
171 FMap (U_b A ccc b) = λ f → CCC._* ccc ( A [ f o CCC.ε ccc ] ) 171 FMap (U_b A ccc b) = λ f → CCC._* ccc ( A [ f o CCC.ε ccc ] )
172 isFunctor (U_b A ccc b) = isF where 172 isFunctor (U_b A ccc b) = isF where
173 isF : IsFunctor A A ( λ a → (CCC._<=_ ccc a b)) ( λ f → CCC._* ccc ( A [ f o CCC.ε ccc ] ) ) 173 _<=_ = CCC._<=_ ccc
174 _∧_ = CCC._∧_ ccc
175 <_,_> = CCC.<_,_> ccc
176 _* = CCC._* ccc
177 ε = CCC.ε ccc
178 π = CCC.π ccc
179 π' = CCC.π' ccc
180 isc = CCC.isCCC ccc
181 *-cong = IsCCC.*-cong (CCC.isCCC ccc)
182 π-cong = IsCCC.π-cong (CCC.isCCC ccc)
183
184 isF : IsFunctor A A ( λ a → (a <= b)) ( λ f → CCC._* ccc ( A [ f o ε ] ) )
174 IsFunctor.≈-cong isF f≈g = IsCCC.*-cong (CCC.isCCC ccc) ( car f≈g ) where open ≈-Reasoning A 185 IsFunctor.≈-cong isF f≈g = IsCCC.*-cong (CCC.isCCC ccc) ( car f≈g ) where open ≈-Reasoning A
175 -- e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ] 186 -- e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ]
176 IsFunctor.identity isF {a} = begin 187 IsFunctor.identity isF {a} = begin
177 (ccc CCC.*) (A [ id1 A a o CCC.ε ccc ]) 188 (id1 A a o ε ) *
178 ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) ( begin 189 ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) ( begin
179 id1 A a o CCC.ε ccc 190 id1 A a o CCC.ε ccc
180 ≈⟨ idL ⟩ 191 ≈⟨ idL ⟩
181 CCC.ε ccc 192 ε
182 ≈↑⟨ idR ⟩ 193 ≈↑⟨ idR ⟩
183 CCC.ε ccc o id1 A (CCC._∧_ ccc ( CCC._<=_ ccc a b ) b ) 194 ε o id1 A ( ( a <= b ) ∧ b )
184 ≈↑⟨ cdr ( IsCCC.π-id (CCC.isCCC ccc)) ⟩ 195 ≈↑⟨ cdr ( IsCCC.π-id isc) ⟩
185 CCC.ε ccc o ( CCC.<_,_> ccc ( CCC.π ccc ) (CCC.π' ccc) ) 196 ε o ( < π , π' > )
186 ≈↑⟨ cdr ( IsCCC.π-cong (CCC.isCCC ccc) idL refl-hom) ⟩ 197 ≈↑⟨ cdr ( π-cong idL refl-hom) ⟩
187 CCC.ε ccc o ( CCC.<_,_> ccc ( id1 A (CCC._<=_ ccc a b) o CCC.π ccc ) (CCC.π' ccc) ) 198 ε o ( < id1 A (a <= b) o π , π' > )
188 ∎ ) ⟩ 199 ∎ ) ⟩
189 (ccc CCC.*) ( CCC.ε ccc o ( CCC.<_,_> ccc ( id1 A (CCC._<=_ ccc a b) o CCC.π ccc ) (CCC.π' ccc) )) 200 ( ε o ( < id1 A ( a <= b) o π , π' > ) ) *
190 ≈⟨ IsCCC.e4b (CCC.isCCC ccc) ⟩ 201 ≈⟨ IsCCC.e4b (CCC.isCCC ccc) ⟩
191 id1 A ((ccc CCC.<= a) b) 202 id1 A (a <= b)
192 ∎ where open ≈-Reasoning A 203 ∎ where open ≈-Reasoning A
193 IsFunctor.distr isF {x} {y} {z} {f} {g} = begin 204 IsFunctor.distr isF {x} {y} {z} {f} {g} = begin
194 (ccc CCC.*) ( ( g o f ) o CCC.ε ccc ) 205 ( ( g o f ) o ε ) *
195 ≈⟨ {!!} ⟩ 206 ≈↑⟨ *-cong assoc ⟩
196 (ccc CCC.*) (( g o CCC.ε ccc ) o CCC.<_,_> ccc ((ccc CCC.*) 207 ( g o (f o ε ) ) *
197 ( f o ( CCC.ε ccc o CCC.<_,_> ccc (CCC.π ccc o CCC.π ccc ) (CCC.π' ccc)))) (CCC.π' ccc)) 208 ≈↑⟨ *-cong ( cdr (IsCCC.e4a isc) ) ⟩
198 ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) ( cdr ( IsCCC.π-cong (CCC.isCCC ccc) ( begin 209 ( g o ( ε o ( < ( ( f o ε ) * ) o π , π' > ) )) *
199 (ccc CCC.*) ( f o ( CCC.ε ccc o CCC.<_,_> ccc (CCC.π ccc o CCC.π ccc ) (CCC.π' ccc))) 210 ≈⟨ *-cong assoc ⟩
200 ≈⟨ IsCCC.*-cong (CCC.isCCC ccc) assoc ⟩ 211 ( ( g o ε ) o ( < ( ( f o ε ) * ) o π , π' > ) ) *
201 (ccc CCC.*) (( f o CCC.ε ccc ) o CCC.<_,_> ccc (CCC.π ccc o CCC.π ccc ) (CCC.π' ccc)) 212 ≈↑⟨ IsCCC.distr-* isc ⟩
202 ≈↑⟨ IsCCC.distr-* (CCC.isCCC ccc) ⟩ 213 ( g o ε ) * o ( f o ε ) *
203 (ccc CCC.*) ( f o CCC.ε ccc ) o CCC.π ccc 214 ∎ where open ≈-Reasoning A
204 ∎ ) refl-hom )) ⟩ 215
205 (ccc CCC.*) (( g o CCC.ε ccc ) o CCC.<_,_> ccc ( (ccc CCC.*) ( f o CCC.ε ccc ) o CCC.π ccc ) (CCC.π' ccc) ) 216 F_b : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( ccc : CCC A ) → (b : Obj A) → Functor A A
206 ≈↑⟨ IsCCC.distr-* (CCC.isCCC ccc) ⟩ 217 FObj (F_b A ccc b) = λ a → ( CCC._∧_ ccc a b )
207 (ccc CCC.*) ( g o CCC.ε ccc ) o (ccc CCC.*) ( f o CCC.ε ccc ) 218 FMap (F_b A ccc b) = λ f → ( CCC.<_,_> ccc (A [ f o CCC.π ccc ] ) ( CCC.π' ccc) )
208 ∎ where open ≈-Reasoning A 219 isFunctor (F_b A ccc b) = isF where
220 _∧_ = CCC._∧_ ccc
221 <_,_> = CCC.<_,_> ccc
222 π = CCC.π ccc
223 π' = CCC.π' ccc
224 isc = CCC.isCCC ccc
225 π-cong = IsCCC.π-cong (CCC.isCCC ccc)
226
227 isF : IsFunctor A A ( λ a → (a ∧ b)) ( λ f → < ( A [ f o π ] ) , π' > )
228 IsFunctor.≈-cong isF f≈g = π-cong ( car f≈g ) refl-hom where open ≈-Reasoning A
229 IsFunctor.identity isF {a} = trans-hom (π-cong idL refl-hom ) (IsCCC.π-id isc) where open ≈-Reasoning A
230 IsFunctor.distr isF {x} {y} {z} {f} {g} = begin
231 < ( g o f ) o π , π' >
232 ≈↑⟨ π-cong assoc refl-hom ⟩
233 < g o ( f o π ) , π' >
234 ≈↑⟨ π-cong (cdr (IsCCC.e3a isc )) refl-hom ⟩
235 < g o ( π o < ( f o π ) , π' > ) , π' >
236 ≈⟨ π-cong assoc ( sym-hom (IsCCC.e3b isc )) ⟩
237 < ( g o π ) o < ( f o π ) , π' > , π' o < ( f o π ) , π' > >
238 ≈↑⟨ IsCCC.distr-π isc ⟩
239 < ( g o π ) , π' > o < ( f o π ) , π' >
240 ∎ where open ≈-Reasoning A
241
242 CCCtoAdj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → (b : Obj A ) → coUniversalMapping A A (F_b A ccc b)
243 CCCtoAdj A ccc b = record {
244 U = λ a → a <= b
245 ; ε = ε'
246 ; _*' = solution
247 ; iscoUniversalMapping = record {
248 couniversalMapping = couniversalMapping
249 ; couniquness = couniquness
250 }
251 } where
252 _<=_ = CCC._<=_ ccc
253 <_,_> = CCC.<_,_> ccc
254 _* = CCC._* ccc
255 ε = CCC.ε ccc
256 π = CCC.π ccc
257 π' = CCC.π' ccc
258 isc = CCC.isCCC ccc
259 *-cong = IsCCC.*-cong (CCC.isCCC ccc)
260 ε' : (a : Obj A) → Hom A (FObj (F_b A ccc b) (a <= b)) a
261 ε' a = ε
262 solution : { b' : Obj A} {a : Obj A} → Hom A (FObj (F_b A ccc b) a) b' → Hom A a (b' <= b)
263 solution f = f *
264 couniversalMapping : {b = b₁ : Obj A} {a : Obj A}
265 {f : Hom A (FObj (F_b A ccc b) a) b₁} →
266 A [ A [ ε' b₁ o FMap (F_b A ccc b) (solution f) ] ≈ f ]
267 couniversalMapping {c} {a} {f} = IsCCC.e4a isc
268 couniquness : {b = b₁ : Obj A} {a : Obj A}
269 {f : Hom A (FObj (F_b A ccc b) a) b₁} {g : Hom A a (b₁ <= b)} →
270 A [ A [ ε' b₁ o FMap (F_b A ccc b) g ] ≈ f ] → A [ solution f ≈ g ]
271 couniquness {c} {a} {f} {g} eq = begin
272 f *
273 ≈↑⟨ *-cong eq ⟩
274 ( ε o FMap (F_b A ccc b) g ) *
275 ≈⟨⟩
276 ( ε o < ( g o π ) , π' > ) *
277 ≈⟨ IsCCC.e4b isc ⟩
278 g
279 ∎ where open ≈-Reasoning A
280
209 281
210 282
211 283
212 c^b=b<=c : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} → -- Hom A １ ( c ^ b ) ≅ Hom A b c 284 c^b=b<=c : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( ccc : CCC A ) → {a b c : Obj A} → -- Hom A １ ( c ^ b ) ≅ Hom A b c
213 IsoS A A (CCC.１ ccc ) (CCC._<=_ ccc c b) b c 285 IsoS A A (CCC.１ ccc ) (CCC._<=_ ccc c b) b c
297 369
298 hom→CCC : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( h : CCChom A ) → CCC A 370 hom→CCC : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( h : CCChom A ) → CCC A
299 hom→CCC A h = record { 371 hom→CCC A h = record {
300 １ = １ 372 １ = １
301 ; ○ = ○ 373 ; ○ = ○
302 ; _∧_ = _/\_ 374 ; _∧_ = _∧_
303 ; <_,_> = <,> 375 ; <_,_> = <,>
304 ; π = π 376 ; π = π
305 ; π' = π' 377 ; π' = π'
306 ; _<=_ = _<=_ 378 ; _<=_ = _<=_
307 ; _* = _* 379 ; _* = _*
310 } where 382 } where
311 １ : Obj A 383 １ : Obj A
312 １ = one h 384 １ = one h
313 ○ : (a : Obj A ) → Hom A a １ 385 ○ : (a : Obj A ) → Hom A a １
314 ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj 386 ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj
315 _/\_ : Obj A → Obj A → Obj A 387 _∧_ : Obj A → Obj A → Obj A
316 _/\_ a b = _*_ h a b 388 _∧_ a b = _*_ h a b
317 <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a /\ b) 389 <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a ∧ b)
318 <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g ) 390 <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g )
319 π : {a b : Obj A } → Hom A (a /\ b) a 391 π : {a b : Obj A } → Hom A (a ∧ b) a
320 π {a} {b} = proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) )) 392 π {a} {b} = proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
321 π' : {a b : Obj A } → Hom A (a /\ b) b 393 π' : {a b : Obj A } → Hom A (a ∧ b) b
322 π' {a} {b} = proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) )) 394 π' {a} {b} = proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
323 _<=_ : (a b : Obj A ) → Obj A 395 _<=_ : (a b : Obj A ) → Obj A
324 _<=_ = _^_ h 396 _<=_ = _^_ h
325 _* : {a b c : Obj A } → Hom A (a /\ b) c → Hom A a (c <= b) 397 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b)
326 _* = ≅← ( ccc-3 (isCCChom h ) ) 398 _* = ≅← ( ccc-3 (isCCChom h ) )
327 ε : {a b : Obj A } → Hom A ((a <= b ) /\ b) a 399 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a
328 ε {a} {b} = ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) 400 ε {a} {b} = ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b ))
329 isCCC : CCC.IsCCC A １ ○ _/\_ <,> π π' _<=_ _* ε 401 isCCC : CCC.IsCCC A １ ○ _∧_ <,> π π' _<=_ _* ε
330 isCCC = record { 402 isCCC = record {
331 e2 = e2 403 e2 = e2
332 ; e3a = e3a 404 ; e3a = e3a
333 ; e3b = e3b 405 ; e3b = e3b
334 ; e3c = e3c 406 ; e3c = e3c
387 ≈⟨ cong-proj₂ ( iso→ (ccc-2 (isCCChom h))) ⟩ 459 ≈⟨ cong-proj₂ ( iso→ (ccc-2 (isCCChom h))) ⟩
388 proj₂ ( f , g ) 460 proj₂ ( f , g )
389 ≈⟨⟩ 461 ≈⟨⟩
390 g 462 g
391 ∎ where open ≈-Reasoning A 463 ∎ where open ≈-Reasoning A
392 e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ] 464 e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ]
393 e3c {a} {b} {c} {f} = begin 465 e3c {a} {b} {c} {f} = begin
394 <,> ( π o f ) ( π' o f ) 466 <,> ( π o f ) ( π' o f )
395 ≈⟨⟩ 467 ≈⟨⟩
396 ≅← (ccc-2 (isCCChom h)) ( ( proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) ))) o f 468 ≅← (ccc-2 (isCCChom h)) ( ( proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) ))) o f
397 , ( proj₂ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b)))) o f ) 469 , ( proj₂ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b)))) o f )
412 ≈⟨ cong← (ccc-2 (isCCChom h)) ( eq1 , eq2 ) ⟩ 484 ≈⟨ cong← (ccc-2 (isCCChom h)) ( eq1 , eq2 ) ⟩
413 ≅← (ccc-2 (isCCChom h)) (f' , g') 485 ≅← (ccc-2 (isCCChom h)) (f' , g')
414 ≈⟨⟩ 486 ≈⟨⟩
415 <,> f' g' 487 <,> f' g'
416 ∎ where open ≈-Reasoning A 488 ∎ where open ≈-Reasoning A
417 e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ] 489 e4a : {a b c : Obj A} → { k : Hom A (c ∧ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ]
418 e4a {a} {b} {c} {k} = begin 490 e4a {a} {b} {c} {k} = begin
419 ε o ( <,> ((k *) o π ) π' ) 491 ε o ( <,> ((k *) o π ) π' )
420 ≈⟨⟩ 492 ≈⟨⟩
421 ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π')) 493 ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π'))
422 ≈⟨ nat-3 (isCCChom h) ⟩ 494 ≈⟨ nat-3 (isCCChom h) ⟩
432 ≈⟨ cong← (ccc-3 (isCCChom h)) (nat-3 (isCCChom h)) ⟩ 504 ≈⟨ cong← (ccc-3 (isCCChom h)) (nat-3 (isCCChom h)) ⟩
433 ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k) 505 ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k)
434 ≈⟨ iso← (ccc-3 (isCCChom h)) ⟩ 506 ≈⟨ iso← (ccc-3 (isCCChom h)) ⟩
435 k 507 k
436 ∎ where open ≈-Reasoning A 508 ∎ where open ≈-Reasoning A
437 *-cong : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ] 509 *-cong : {a b c : Obj A} {f f' : Hom A (a ∧ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
438 *-cong eq = cong← ( ccc-3 (isCCChom h )) eq 510 *-cong eq = cong← ( ccc-3 (isCCChom h )) eq
439 511
440 open import Category.Sets 512 open import Category.Sets
441 513
442 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ 514 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
446 518
447 sets : {l : Level } → CCC (Sets {l}) 519 sets : {l : Level } → CCC (Sets {l})
448 sets {l} = record { 520 sets {l} = record {
449 １ = One' 521 １ = One'
450 ; ○ = λ _ → λ _ → OneObj' 522 ; ○ = λ _ → λ _ → OneObj'
451 ; _∧_ = _/\_ 523 ; _∧_ = _∧_
452 ; <_,_> = <,> 524 ; <_,_> = <,>
453 ; π = π 525 ; π = π
454 ; π' = π' 526 ; π' = π'
455 ; _<=_ = _<=_ 527 ; _<=_ = _<=_
456 ; _* = _* 528 ; _* = _*
459 } where 531 } where
460 １ : Obj Sets 532 １ : Obj Sets
461 １ = One' 533 １ = One'
462 ○ : (a : Obj Sets ) → Hom Sets a １ 534 ○ : (a : Obj Sets ) → Hom Sets a １
463 ○ a = λ _ → OneObj' 535 ○ a = λ _ → OneObj'
464 _/\_ : Obj Sets → Obj Sets → Obj Sets 536 _∧_ : Obj Sets → Obj Sets → Obj Sets
465 _/\_ a b = a ∧ b 537 _∧_ a b = a /\ b
466 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a /\ b) 538 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b)
467 <,> f g = λ x → ( f x , g x ) 539 <,> f g = λ x → ( f x , g x )
468 π : {a b : Obj Sets } → Hom Sets (a /\ b) a 540 π : {a b : Obj Sets } → Hom Sets (a ∧ b) a
469 π {a} {b} = proj₁ 541 π {a} {b} = proj₁
470 π' : {a b : Obj Sets } → Hom Sets (a /\ b) b 542 π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b
471 π' {a} {b} = proj₂ 543 π' {a} {b} = proj₂
472 _<=_ : (a b : Obj Sets ) → Obj Sets 544 _<=_ : (a b : Obj Sets ) → Obj Sets
473 a <= b = b → a 545 a <= b = b → a
474 _* : {a b c : Obj Sets } → Hom Sets (a /\ b) c → Hom Sets a (c <= b) 546 _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b)
475 f * = λ x → λ y → f ( x , y ) 547 f * = λ x → λ y → f ( x , y )
476 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) /\ b) a 548 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a
477 ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x ) 549 ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x )
478 isCCC : CCC.IsCCC Sets １ ○ _/\_ <,> π π' _<=_ _* ε 550 isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε
479 isCCC = record { 551 isCCC = record {
480 e2 = e2 552 e2 = e2
481 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g} 553 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g}
482 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g} 554 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g}
483 ; e3c = e3c 555 ; e3c = e3c
496 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ] 568 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ]
497 e3a = refl 569 e3a = refl
498 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} → 570 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
499 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ] 571 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ]
500 e3b = refl 572 e3b = refl
501 e3c : {a b c : Obj Sets} {h : Hom Sets c (a /\ b)} → 573 e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} →
502 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ] 574 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ]
503 e3c = refl 575 e3c = refl
504 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} → 576 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
505 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ] 577 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ]
506 π-cong refl refl = refl 578 π-cong refl refl = refl
507 e4a : {a b c : Obj Sets} {h : Hom Sets (c /\ b) a} → 579 e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} →
508 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ] 580 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ]
509 e4a = refl 581 e4a = refl
510 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} → 582 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} →
511 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ] 583 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ]
512 e4b = refl 584 e4b = refl
513 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a /\ b) c} → 585 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} →
514 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] 586 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
515 *-cong refl = refl 587 *-cong refl = refl
516 588
517 589