Mercurial > hg > Members > kono > Proof > category
comparison CCChom.agda @ 784:f27d966939f8
add CCC hom
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 17 Apr 2019 14:47:39 +0900 |
parents | CCC.agda@bded2347efa4 |
children | a67959bcd44b |
comparison
equal
deleted
inserted
replaced
783:bded2347efa4 | 784:f27d966939f8 |
---|---|
1 open import Level | |
2 open import Category | |
3 module CCChom where | |
4 | |
5 open import HomReasoning | |
6 open import cat-utility | |
7 open import Data.Product renaming (_×_ to _∧_) | |
8 open import Category.Constructions.Product | |
9 open import Relation.Binary.PropositionalEquality | |
10 | |
11 open Functor | |
12 | |
13 -- ccc-1 : Hom A a 1 ≅ {*} | |
14 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) | |
15 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c | |
16 | |
17 data One {c : Level} : Set c where | |
18 OneObj : One -- () in Haskell ( or any one object set ) | |
19 | |
20 OneCat : Category Level.zero Level.zero Level.zero | |
21 OneCat = record { | |
22 Obj = One ; | |
23 Hom = λ a b → One ; | |
24 _o_ = λ{a} {b} {c} x y → OneObj ; | |
25 _≈_ = λ x y → x ≡ y ; | |
26 Id = λ{a} → OneObj ; | |
27 isCategory = record { | |
28 isEquivalence = record {refl = refl ; trans = trans ; sym = sym } ; | |
29 identityL = λ{a b f} → lemma {a} {b} {f} ; | |
30 identityR = λ{a b f} → lemma {a} {b} {f} ; | |
31 o-resp-≈ = λ{a b c f g h i} _ _ → refl ; | |
32 associative = λ{a b c d f g h } → refl | |
33 } | |
34 } where | |
35 lemma : {a b : One {Level.zero}} → { f : One {Level.zero}} → OneObj ≡ f | |
36 lemma {a} {b} {f} with f | |
37 ... | OneObj = refl | |
38 | |
39 record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) | |
40 : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where | |
41 field | |
42 ≅→ : Hom A a b → Hom B a' b' | |
43 ≅← : Hom B a' b' → Hom A a b | |
44 iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] | |
45 iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] | |
46 | |
47 | |
48 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (1 : Obj A) | |
49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where | |
50 field | |
51 ccc-1 : {a : Obj A} → -- Hom A a 1 ≅ {*} | |
52 IsoS A OneCat a 1 OneObj OneObj | |
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 | |
57 | |
58 | |
59 record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where | |
60 field | |
61 one : Obj A | |
62 _*_ : Obj A → Obj A → Obj A | |
63 _^_ : Obj A → Obj A → Obj A | |
64 isCCChom : IsCCChom A one _*_ _^_ | |
65 | |
66 open import HomReasoning | |
67 | |
68 open import CCC | |
69 | |
70 CCC→hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( c : CCC A ) → CCChom A | |
71 CCC→hom A c = record { | |
72 one = CCC.1 c | |
73 ; _*_ = CCC._∧_ c | |
74 ; _^_ = CCC._<=_ c | |
75 ; isCCChom = record { | |
76 ccc-1 = {!!} | |
77 ; ccc-2 = {!!} | |
78 ; ccc-3 = {!!} | |
79 } | |
80 } |