Mercurial > hg > Members > kono > Proof > category

comparison CCChom.agda @ 790:1e7319868d77

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sets is CCC
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Apr 2019 23:42:19 +0900
parents 4e1e2f7199c8
children f37f11e1b871
comparison
equal deleted inserted replaced
789:4e1e2f7199c8 790:1e7319868d77
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 _∧_)
8 open import Category.Constructions.Product 8 open import Category.Constructions.Product
9 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
10 10
11 open Functor 11 open Functor
12 12
13 -- ccc-1 : Hom A a 1 ≅ {*} 13 -- ccc-1 : Hom A a 1 ≅ {*}
14 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) 14 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
312 k 312 k
313 ∎ where open ≈-Reasoning A 313 ∎ where open ≈-Reasoning A
314 *-cong : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ] 314 *-cong : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
315 *-cong eq = cong← ( ccc-3 (isCCChom h )) eq 315 *-cong eq = cong← ( ccc-3 (isCCChom h )) eq
316 316
317 317 open import Category.Sets
318 318
319 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
320
321 data One' {l : Level} : Set l where
322 OneObj' : One' -- () in Haskell ( or any one object set )
323
324 sets : {l : Level } → CCC (Sets {l})
325 sets {l} = record {
326 １ = One'
327 ; ○ = λ _ → λ _ → OneObj'
328 ; _∧_ = _/\_
329 ; <_,_> = <,>
330 ; π = π
331 ; π' = π'
332 ; _<=_ = _<=_
333 ; _* = _*
334 ; ε = ε
335 ; isCCC = isCCC
336 } where
337 １ : Obj Sets
338 １ = One'
339 ○ : (a : Obj Sets ) → Hom Sets a １
340 ○ a = λ _ → OneObj'
341 _/\_ : Obj Sets → Obj Sets → Obj Sets
342 _/\_ a b = a ∧ b
343 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a /\ b)
344 <,> f g = λ x → ( f x , g x )
345 π : {a b : Obj Sets } → Hom Sets (a /\ b) a
346 π {a} {b} = proj₁
347 π' : {a b : Obj Sets } → Hom Sets (a /\ b) b
348 π' {a} {b} = proj₂
349 _<=_ : (a b : Obj Sets ) → Obj Sets
350 a <= b = b → a
351 _* : {a b c : Obj Sets } → Hom Sets (a /\ b) c → Hom Sets a (c <= b)
352 f * = λ x → λ y → f ( x , y )
353 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) /\ b) a
354 ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x )
355 isCCC : CCC.IsCCC Sets １ ○ _/\_ <,> π π' _<=_ _* ε
356 isCCC = record {
357 e2 = e2
358 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g}
359 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g}
360 ; e3c = e3c
361 ; π-cong = π-cong
362 ; e4a = e4a
363 ; e4b = e4b
364 ; *-cong = *-cong
365 } where
366 e2 : {a : Obj Sets} (f : Hom Sets a １) → Sets [ f ≈ ○ a ]
367 e2 {a} f = extensionality Sets ( λ x → e20 x )
368 where
369 e20 : (x : a ) → f x ≡ ○ a x
370 e20 x with f x
371 e20 x | OneObj' = refl
372 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
373 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ]
374 e3a = refl
375 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
376 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ]
377 e3b = refl
378 e3c : {a b c : Obj Sets} {h : Hom Sets c (a /\ b)} →
379 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ]
380 e3c = refl
381 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
382 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ]
383 π-cong refl refl = refl
384 e4a : {a b c : Obj Sets} {h : Hom Sets (c /\ b) a} →
385 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ]
386 e4a = refl
387 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} →
388 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ]
389 e4b = refl
390 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a /\ b) c} →
391 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
392 *-cong refl = refl
393
394