Mercurial > hg > Members > kono > Proof > category
comparison CCC.agda @ 780:b44c1c6ce646
CCC in Hom form
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 08 Oct 2018 16:48:27 +0900 |
parents | 6b4bd02efd80 |
children | 340708e8d54f |
comparison
equal
deleted
inserted
replaced
779:6b4bd02efd80 | 780:b44c1c6ce646 |
---|---|
2 open import Category | 2 open import Category |
3 module CCC where | 3 module CCC 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 _∧_) |
8 open import Category.Constructions.Product | |
9 open import Relation.Binary.PropositionalEquality | |
8 | 10 |
9 open Functor | 11 open Functor |
10 | 12 |
11 -- ccc-1 : Hom A a 1 ≅ {*} | 13 -- ccc-1 : Hom A a 1 ≅ {*} |
12 -- 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 ) |
13 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c | 15 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c |
14 | 16 |
15 record _≅_ {c₁ c₂ ℓ ℓ' : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A} (f : Hom A a b) (S : Set ℓ') : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ ℓ' ) where | 17 record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) |
18 : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where | |
16 field | 19 field |
17 ≅→ : {!!} | 20 ≅→ : Hom A a b → Hom B a' b' |
18 ≅← : {!!} | 21 ≅← : Hom B a' b' → Hom A a b |
19 iso→ : {!!} | 22 iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] |
20 iso← : {!!} | 23 iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] |
21 | 24 |
22 data One {c : Level} : Set c where | 25 data One {c : Level} : Set c where |
23 OneObj : One -- () in Haskell ( or any one object set ) | 26 OneObj : One -- () in Haskell ( or any one object set ) |
24 | 27 |
28 OneCat : Category Level.zero Level.zero Level.zero | |
29 OneCat = record { | |
30 Obj = One ; | |
31 Hom = λ a b → One ; | |
32 _o_ = λ{a} {b} {c} x y → OneObj ; | |
33 _≈_ = λ x y → x ≡ y ; | |
34 Id = λ{a} → OneObj ; | |
35 isCategory = record { | |
36 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; | |
37 identityL = λ{a b f} → lemma {a} {b} {f} ; | |
38 identityR = λ{a b f} → lemma {a} {b} {f} ; | |
39 o-resp-≈ = λ{a b c f g h i} _ _ → refl ; | |
40 associative = λ{a b c d f g h } → refl | |
41 } | |
42 } where | |
43 lemma : {a b : One {Level.zero}} → { f : One {Level.zero}} → OneObj ≡ f | |
44 lemma {a} {b} {f} with f | |
45 ... | OneObj = refl | |
46 | |
25 | 47 |
26 record isCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A) | 48 record isCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A) |
27 ( _×_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where | 49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where |
28 field | 50 field |
29 ccc-1 : {a : Obj A} → Hom A a one ≅ One {ℓ} | 51 ccc-1 : {a : Obj A} → -- Hom A a one ≅ {*} |
30 ccc-2 : {a b c : Obj A} → Hom A c ( a × b ) ≅ ( Hom A c a ) * ( Hom A c b ) | 52 IsoS A OneCat a one OneObj OneObj |
31 ccc-3 : {a b c : Obj A} → Hom A a ( c ^ b ) ≅ Hom A ( a × b ) c | 53 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b ) |
54 IsoS A (A × A) c (a * b) (c , c) (a , b) | |
55 ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c | |
56 IsoS A A a (c ^ b) (a * b) c | |
32 | 57 |
33 | 58 |
34 | 59 |