|
999
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 module CCCSets where
|
|
|
3
|
|
|
4 open import Level
|
|
|
5 open import Category
|
|
|
6 open import HomReasoning
|
|
|
7 open import cat-utility
|
|
|
8 open import Data.Product renaming (_×_ to _/\_ ) hiding ( <_,_> )
|
|
|
9 open import Category.Constructions.Product
|
|
|
10 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
11 open import CCC
|
|
|
12
|
|
|
13 open Functor
|
|
|
14
|
|
|
15 -- ccc-1 : Hom A a 1 ≅ {*}
|
|
|
16 -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
|
|
|
17 -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c
|
|
|
18
|
|
|
19 open import Category.Sets
|
|
|
20
|
|
|
21 -- Sets is a CCC
|
|
|
22
|
|
1018
|
23 open import SetsCompleteness hiding (ki1)
|
|
|
24
|
|
|
25 -- import Axiom.Extensionality.Propositional
|
|
|
26 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂
|
|
999
|
27
|
|
|
28 data One {c : Level } : Set c where
|
|
|
29 OneObj : One -- () in Haskell ( or any one object set )
|
|
|
30
|
|
|
31 sets : {c : Level } → CCC (Sets {c})
|
|
|
32 sets = record {
|
|
|
33 １ = One
|
|
|
34 ; ○ = λ _ → λ _ → OneObj
|
|
|
35 ; _∧_ = _∧_
|
|
|
36 ; <_,_> = <,>
|
|
|
37 ; π = π
|
|
|
38 ; π' = π'
|
|
|
39 ; _<=_ = _<=_
|
|
|
40 ; _* = _*
|
|
|
41 ; ε = ε
|
|
|
42 ; isCCC = isCCC
|
|
|
43 } where
|
|
|
44 １ : Obj Sets
|
|
|
45 １ = One
|
|
|
46 ○ : (a : Obj Sets ) → Hom Sets a １
|
|
|
47 ○ a = λ _ → OneObj
|
|
|
48 _∧_ : Obj Sets → Obj Sets → Obj Sets
|
|
|
49 _∧_ a b = a /\ b
|
|
|
50 <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b)
|
|
|
51 <,> f g = λ x → ( f x , g x )
|
|
|
52 π : {a b : Obj Sets } → Hom Sets (a ∧ b) a
|
|
|
53 π {a} {b} = proj₁
|
|
|
54 π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b
|
|
|
55 π' {a} {b} = proj₂
|
|
|
56 _<=_ : (a b : Obj Sets ) → Obj Sets
|
|
|
57 a <= b = b → a
|
|
|
58 _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b)
|
|
|
59 f * = λ x → λ y → f ( x , y )
|
|
|
60 ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a
|
|
|
61 ε {a} {b} = λ x → ( proj₁ x ) ( proj₂ x )
|
|
|
62 isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε
|
|
|
63 isCCC = record {
|
|
|
64 e2 = e2
|
|
|
65 ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g}
|
|
|
66 ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g}
|
|
|
67 ; e3c = e3c
|
|
|
68 ; π-cong = π-cong
|
|
|
69 ; e4a = e4a
|
|
|
70 ; e4b = e4b
|
|
|
71 ; *-cong = *-cong
|
|
|
72 } where
|
|
|
73 e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ]
|
|
|
74 e2 {a} {f} = extensionality Sets ( λ x → e20 x )
|
|
|
75 where
|
|
|
76 e20 : (x : a ) → f x ≡ ○ a x
|
|
|
77 e20 x with f x
|
|
|
78 e20 x | OneObj = refl
|
|
|
79 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
|
|
|
80 Sets [ ( Sets [ π o ( <,> f g) ] ) ≈ f ]
|
|
|
81 e3a = refl
|
|
|
82 e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
|
|
|
83 Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ]
|
|
|
84 e3b = refl
|
|
|
85 e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} →
|
|
|
86 Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ]
|
|
|
87 e3c = refl
|
|
|
88 π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
|
|
|
89 Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ]
|
|
|
90 π-cong refl refl = refl
|
|
|
91 e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} →
|
|
|
92 Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ]
|
|
|
93 e4a = refl
|
|
|
94 e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} →
|
|
|
95 Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ]
|
|
|
96 e4b = refl
|
|
|
97 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} →
|
|
|
98 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
|
|
|
99 *-cong refl = refl
|
|
|
100
|
|
|
101 -- ○ b
|
|
|
102 -- b -----------→ 1
|
|
|
103 -- | |
|
|
|
104 -- m | | ⊤
|
|
|
105 -- ↓ char m ↓
|
|
|
106 -- a -----------→ Ω
|
|
|
107 -- h
|
|
|
108
|
|
1010
|
109 data Bool {c : Level } : Set c where
|
|
|
110 true : Bool
|
|
|
111 false : Bool
|
|
999
|
112
|
|
1018
|
113 -- data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where
|
|
|
114 -- elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g
|
|
999
|
115
|
|
1018
|
116 -- irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq'
|
|
|
117 -- irr refl refl = refl
|
|
999
|
118
|
|
|
119 topos : {c : Level } → Topos (Sets {c}) sets
|
|
|
120 topos {c} = record {
|
|
1010
|
121 Ω = Bool
|
|
999
|
122 ; ⊤ = λ _ → true
|
|
|
123 ; Ker = tker
|
|
|
124 ; char = tchar
|
|
|
125 ; isTopos = record {
|
|
1018
|
126 char-uniqueness = λ {a} {b} {h} m mono → extensionality Sets ( λ x → uniq h m mono x )
|
|
|
127 ; ker-m = imequ
|
|
999
|
128 }
|
|
|
129 } where
|
|
1010
|
130 tker : {a : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true) o CCC.○ sets a ])
|
|
999
|
131 tker {a} h = record {
|
|
1018
|
132 equalizer-c = sequ a Bool h (λ _ → true)
|
|
|
133 ; equalizer = λ e → equ e
|
|
|
134 ; isEqualizer = SetsIsEqualizer _ _ _ _ }
|
|
1010
|
135 tchar : {a b : Obj Sets} (m : Hom Sets b a) → Mono Sets m → Hom Sets a Bool
|
|
999
|
136 tchar {a} {b} m mono x = true
|
|
1018
|
137 selem : {a : Obj (Sets {c})} → (x : sequ a Bool (λ x₁ → true) (λ _ → true)) → a
|
|
|
138 selem (elem x eq) = x
|
|
|
139 imequ : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true) o CCC.○ sets a ])
|
|
|
140 imequ {a} {b} m mono = record {
|
|
|
141 fe=ge = extensionality Sets ( λ x → refl )
|
|
|
142 ; k = λ h eq → {!!}
|
|
|
143 ; ek=h = {!!}
|
|
|
144 ; uniqueness = {!!}
|
|
|
145 }
|
|
1010
|
146 uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (x : a) → true ≡ h x
|
|
|
147 uniq {a} {b} h m mono x = begin
|
|
|
148 true ≡⟨⟩
|
|
1016
|
149 (λ × → true ) x ≡⟨ cong (λ k → {!!} ) (sym (IsEqualizer.fe=ge (Equalizer.isEqualizer (tker h)) ) ) ⟩
|
|
|
150 {!!} ≡⟨ {!!} ⟩
|
|
1010
|
151 h x ∎ where
|
|
|
152 open ≡-Reasoning
|
|
1016
|
153 yy : Sets [ (λ e → {!!} ) ≈ (λ e → true) ]
|
|
|
154 yy = IsEqualizer.fe=ge (Equalizer.isEqualizer (tker h))
|
|
1010
|
155 yyy : {c : Obj Sets } → (f g : c → b ) → Sets [ Sets [ m o f ] ≈ Sets [ m o g ] ] → f ≡ g
|
|
|
156 yyy f g eq = Mono.isMono mono f g eq
|
|
|
157 yyy1 : {c : Obj Sets } → (f g : c → b ) → Sets [ Sets [ m o f ] ≈ Sets [ m o g ] ] → f ≡ g
|
|
|
158 yyy1 f g eq = Mono.isMono mono f g eq
|
|
|
159
|
|
|
160
|
|
999
|
161
|
|
|
162 open import graph
|
|
|
163 module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where
|
|
|
164
|
|
|
165 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
|
|
|
166 open Graph
|
|
|
167
|
|
|
168 V = vertex G
|
|
|
169 E : V → V → Set c₂
|
|
|
170 E = edge G
|
|
|
171
|
|
|
172 data Objs : Set c₁ where
|
|
|
173 atom : V → Objs
|
|
|
174 ⊤ : Objs
|
|
|
175 _∧_ : Objs → Objs → Objs
|
|
|
176 _<=_ : Objs → Objs → Objs
|
|
|
177
|
|
|
178 data Arrows : (b c : Objs ) → Set (c₁ ⊔ c₂)
|
|
|
179 data Arrow : Objs → Objs → Set (c₁ ⊔ c₂) where --- case i
|
|
|
180 arrow : {a b : V} → E a b → Arrow (atom a) (atom b)
|
|
|
181 π : {a b : Objs } → Arrow ( a ∧ b ) a
|
|
|
182 π' : {a b : Objs } → Arrow ( a ∧ b ) b
|
|
|
183 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
|
|
|
184 _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v
|
|
|
185
|
|
|
186 data Arrows where
|
|
|
187 id : ( a : Objs ) → Arrows a a --- case i
|
|
|
188 ○ : ( a : Objs ) → Arrows a ⊤ --- case i
|
|
|
189 <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b) -- case iii
|
|
|
190 iv : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c -- cas iv
|
|
|
191
|
|
|
192 _・_ : {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
|
|
|
193 id a ・ g = g
|
|
|
194 ○ a ・ g = ○ _
|
|
|
195 < f , g > ・ h = < f ・ h , g ・ h >
|
|
|
196 iv f g ・ h = iv f ( g ・ h )
|
|
|
197
|
|
|
198
|
|
|
199 identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
|
|
|
200 identityL = refl
|
|
|
201
|
|
|
202 identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
|
|
|
203 identityR {a} {a} {id a} = refl
|
|
|
204 identityR {a} {⊤} {○ a} = refl
|
|
|
205 identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR
|
|
|
206 identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR
|
|
|
207
|
|
|
208 assoc≡ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
|
|
|
209 (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
|
|
|
210 assoc≡ (id a) g h = refl
|
|
|
211 assoc≡ (○ a) g h = refl
|
|
|
212 assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h)
|
|
|
213 assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h )
|
|
|
214
|
|
|
215 -- positive intutionistic calculus
|
|
|
216 PL : Category c₁ (c₁ ⊔ c₂) (c₁ ⊔ c₂)
|
|
|
217 PL = record {
|
|
|
218 Obj = Objs;
|
|
|
219 Hom = λ a b → Arrows a b ;
|
|
|
220 _o_ = λ{a} {b} {c} x y → x ・ y ;
|
|
|
221 _≈_ = λ x y → x ≡ y ;
|
|
|
222 Id = λ{a} → id a ;
|
|
|
223 isCategory = record {
|
|
|
224 isEquivalence = record {refl = refl ; trans = trans ; sym = sym} ;
|
|
|
225 identityL = λ {a b f} → identityL {a} {b} {f} ;
|
|
|
226 identityR = λ {a b f} → identityR {a} {b} {f} ;
|
|
|
227 o-resp-≈ = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;
|
|
|
228 associative = λ{a b c d f g h } → assoc≡ f g h
|
|
|
229 }
|
|
|
230 } where
|
|
|
231 o-resp-≈ : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
|
|
|
232 f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
|
|
|
233 o-resp-≈ refl refl = refl
|
|
|
234 --------
|
|
|
235 --
|
|
|
236 -- Functor from Positive Logic to Sets
|
|
|
237 --
|
|
|
238
|
|
|
239 -- open import Category.Sets
|
|
|
240 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂
|
|
|
241
|
|
|
242 open import Data.List
|
|
|
243
|
|
|
244 C = graphtocat.Chain G
|
|
|
245
|
|
|
246 tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
|
|
|
247 tr f x y = graphtocat.next f (x y)
|
|
|
248
|
|
|
249 fobj : ( a : Objs ) → Set (c₁ ⊔ c₂)
|
|
|
250 fobj (atom x) = ( y : vertex G ) → C y x
|
|
|
251 fobj ⊤ = One
|
|
|
252 fobj (a ∧ b) = ( fobj a /\ fobj b)
|
|
|
253 fobj (a <= b) = fobj b → fobj a
|
|
|
254
|
|
|
255 fmap : { a b : Objs } → Hom PL a b → fobj a → fobj b
|
|
|
256 amap : { a b : Objs } → Arrow a b → fobj a → fobj b
|
|
|
257 amap (arrow x) y = tr x y -- tr x
|
|
|
258 amap π ( x , y ) = x
|
|
|
259 amap π' ( x , y ) = y
|
|
|
260 amap ε (f , x ) = f x
|
|
|
261 amap (f *) x = λ y → fmap f ( x , y )
|
|
|
262 fmap (id a) x = x
|
|
|
263 fmap (○ a) x = OneObj
|
|
|
264 fmap < f , g > x = ( fmap f x , fmap g x )
|
|
|
265 fmap (iv x f) a = amap x ( fmap f a )
|
|
|
266
|
|
|
267 -- CS is a map from Positive logic to Sets
|
|
|
268 -- Sets is CCC, so we have a cartesian closed category generated by a graph
|
|
|
269 -- as a sub category of Sets
|
|
|
270
|
|
|
271 CS : Functor PL (Sets {c₁ ⊔ c₂})
|
|
|
272 FObj CS a = fobj a
|
|
|
273 FMap CS {a} {b} f = fmap {a} {b} f
|
|
|
274 isFunctor CS = isf where
|
|
|
275 _+_ = Category._o_ PL
|
|
|
276 ++idR = IsCategory.identityR ( Category.isCategory PL )
|
|
|
277 distr : {a b c : Obj PL} { f : Hom PL a b } { g : Hom PL b c } → (z : fobj a ) → fmap (g + f) z ≡ fmap g (fmap f z)
|
|
|
278 distr {a} {a₁} {a₁} {f} {id a₁} z = refl
|
|
|
279 distr {a} {a₁} {⊤} {f} {○ a₁} z = refl
|
|
|
280 distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k → j , k ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z)
|
|
|
281 distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr {a} {b} {d} {f} {g} z) x where
|
|
|
282 adistr : fmap (g + f) z ≡ fmap g (fmap f z) →
|
|
|
283 ( x : Arrow d c ) → fmap ( iv x (g + f) ) z ≡ fmap ( iv x g ) (fmap f z )
|
|
|
284 adistr eq x = cong ( λ k → amap x k ) eq
|
|
|
285 isf : IsFunctor PL Sets fobj fmap
|
|
|
286 IsFunctor.identity isf = extensionality Sets ( λ x → refl )
|
|
|
287 IsFunctor.≈-cong isf refl = refl
|
|
|
288 IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z )
|
|
|
289
|
|
|
290
|
