779
|
1 open import Level
|
|
2 open import Category
|
784
|
3 module CCChom where
|
779
|
4
|
|
5 open import HomReasoning
|
|
6 open import cat-utility
|
784
|
7 open import Data.Product renaming (_×_ to _∧_)
|
|
8 open import Category.Constructions.Product
|
780
|
9 open import Relation.Binary.PropositionalEquality
|
779
|
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
|
785
|
17 data One : Set where
|
779
|
18 OneObj : One -- () in Haskell ( or any one object set )
|
|
19
|
780
|
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
|
785
|
35 lemma : {a b : One } → { f : One } → OneObj ≡ f
|
780
|
36 lemma {a} {b} {f} with f
|
|
37 ... | OneObj = refl
|
|
38
|
783
|
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 ]
|
779
|
46
|
783
|
47
|
784
|
48 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (1 : Obj A)
|
780
|
49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
779
|
50 field
|
785
|
51 ccc-1 : {a : Obj A} {b c : Obj OneCat} → -- Hom A a 1 ≅ {*}
|
|
52 IsoS A OneCat a 1 b c
|
780
|
53 ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b )
|
784
|
54 IsoS A (A × A) c (a * b) (c , c ) (a , b )
|
780
|
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
|
779
|
57
|
|
58
|
784
|
59 record CCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
781
|
60 field
|
|
61 one : Obj A
|
|
62 _*_ : Obj A → Obj A → Obj A
|
|
63 _^_ : Obj A → Obj A → Obj A
|
784
|
64 isCCChom : IsCCChom A one _*_ _^_
|
783
|
65
|
|
66 open import HomReasoning
|
|
67
|
784
|
68 open import CCC
|
779
|
69
|
784
|
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 {
|
785
|
76 ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 }
|
|
77 ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 }
|
|
78 ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 }
|
784
|
79 }
|
785
|
80 } where
|
|
81 c101 : {a : Obj A} → Hom A a (CCC.1 c) → Hom OneCat OneObj OneObj
|
|
82 c101 _ = OneObj
|
|
83 c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.1 c)
|
|
84 c102 {a} OneObj = CCC.○ c a
|
|
85 c103 : {a : Obj A } {b c : Obj OneCat} {f : Hom OneCat b b } → _[_≈_] OneCat {b} {c} ( c101 {a} (c102 {a} f) ) f
|
|
86 c103 {a} {OneObj} {OneObj} {OneObj} = refl
|
|
87 c104 : {a : Obj A} → {f : Hom A a (CCC.1 c)} → A [ (c102 ( c101 f )) ≈ f ]
|
|
88 c104 {a} {f} = let open ≈-Reasoning A in HomReasoning.≈-Reasoning.sym A (IsCCC.e2 (CCC.isCCC c) f )
|
|
89 c201 : { c₁ a b : Obj A} → Hom A c₁ ((c CCC.∧ a) b) → Hom (A × A) (c₁ , c₁) (a , b)
|
|
90 c201 f = ( A [ CCC.π c o f ] , A [ CCC.π' c o f ] )
|
|
91 c202 : { c₁ a b : Obj A} → Hom (A × A) (c₁ , c₁) (a , b) → Hom A c₁ ((c CCC.∧ a) b)
|
|
92 c202 (f , g ) = CCC.<_,_> c f g
|
|
93 c203 : { c₁ a b : Obj A} → {f : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ (c201 ( c202 f )) ≈ f ]
|
|
94 c203 = ( IsCCC.e3a (CCC.isCCC c) , IsCCC.e3b (CCC.isCCC c))
|
|
95 c204 : { c₁ a b : Obj A} → {f : Hom A c₁ ((c CCC.∧ a) b)} → A [ (c202 ( c201 f )) ≈ f ]
|
|
96 c204 = IsCCC.e3c (CCC.isCCC c)
|
|
97 c301 : { d a b : Obj A} → Hom A a ((c CCC.<= d) b) → Hom A ((c CCC.∧ a) b) d -- a -> d <= b -> (a ∧ b ) -> d
|
|
98 c301 {d} {a} {b} f = A [ CCC.ε c o CCC.<_,_> c ( A [ f o CCC.π c ] ) ( CCC.π' c ) ]
|
|
99 c302 : { d a b : Obj A} → Hom A ((c CCC.∧ a) b) d → Hom A a ((c CCC.<= d) b)
|
|
100 c302 f = CCC._* c f
|
|
101 c303 : { c₁ a b : Obj A} → {f : Hom A ((c CCC.∧ a) b) c₁} → A [ (c301 ( c302 f )) ≈ f ]
|
|
102 c303 = IsCCC.e4a (CCC.isCCC c)
|
|
103 c304 : { c₁ a b : Obj A} → {f : Hom A a ((c CCC.<= c₁) b)} → A [ (c302 ( c301 f )) ≈ f ]
|
|
104 c304 = IsCCC.e4b (CCC.isCCC c)
|
|
105
|
|
106 open CCChom
|
|
107 open IsCCChom
|
|
108 open IsoS
|
|
109
|
|
110 hom→CCC : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( h : CCChom A ) → CCC A
|
|
111 hom→CCC A h = record {
|
|
112 1 = 1
|
|
113 ; ○ = ○
|
|
114 ; _∧_ = _/\_
|
|
115 ; <_,_> = <,>
|
|
116 ; π = π
|
|
117 ; π' = π'
|
|
118 ; _<=_ = _<=_
|
|
119 ; _* = _*
|
|
120 ; ε = ε
|
|
121 ; isCCC = isCCC
|
|
122 } where
|
|
123 1 : Obj A
|
|
124 1 = one h
|
|
125 ○ : (a : Obj A ) → Hom A a 1
|
|
126 ○ a = ≅← ( ccc-1 (isCCChom h ) {_} {OneObj} {OneObj} ) OneObj
|
|
127 _/\_ : Obj A → Obj A → Obj A
|
|
128 _/\_ a b = _*_ h a b
|
|
129 <,> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c ( a /\ b)
|
|
130 <,> f g = ≅← ( ccc-2 (isCCChom h ) ) ( f , g )
|
|
131 π : {a b : Obj A } → Hom A (a /\ b) a
|
|
132 π {a} {b} = proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
|
|
133 π' : {a b : Obj A } → Hom A (a /\ b) b
|
|
134 π' {a} {b} = proj₂ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h a b) ))
|
|
135 _<=_ : (a b : Obj A ) → Obj A
|
|
136 _<=_ = _^_ h
|
|
137 _* : {a b c : Obj A } → Hom A (a /\ b) c → Hom A a (c <= b)
|
|
138 _* = ≅← ( ccc-3 (isCCChom h ) )
|
|
139 ε : {a b : Obj A } → Hom A ((a <= b ) /\ b) a
|
|
140 ε {a} {b} = ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b ))
|
|
141 isCCC : CCC.IsCCC A 1 ○ _/\_ <,> π π' _<=_ _* ε
|
|
142 isCCC = record {
|
|
143 e2 = e2
|
|
144 ; e3a = e3a
|
|
145 ; e3b = e3b
|
|
146 ; e3c = e3c
|
|
147 ; π-cong = π-cong
|
|
148 ; e4a = e4a
|
|
149 ; e4b = e4b
|
|
150 } where
|
|
151 e2 : {a : Obj A} → ∀ ( f : Hom A a 1 ) → A [ f ≈ ○ a ]
|
|
152 e2 f = {!!}
|
|
153 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o <,> f g ] ≈ f ]
|
|
154 e3a = {!!}
|
|
155 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o <,> f g ] ≈ g ]
|
|
156 e3b = {!!}
|
|
157 e3c : {a b c : Obj A} → { h : Hom A c (a /\ b) } → A [ <,> ( A [ π o h ] ) ( A [ π' o h ] ) ≈ h ]
|
|
158 e3c = {!!}
|
|
159 π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ <,> f g ≈ <,> f' g' ]
|
|
160 π-cong = {!!}
|
|
161 e4a : {a b c : Obj A} → { h : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (h *) o π ] ) π') ] ≈ h ]
|
|
162 e4a = {!!}
|
|
163 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ]
|
|
164 e4b = {!!}
|
|
165
|