Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph.agda @ 931:98b5fafb1efb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 12 May 2020 15:56:48 +0900
parents 327abed926d6
children f19425b54aba
comparison
equal deleted inserted replaced
930:327abed926d6 931:98b5fafb1efb
19 19
20 -- Sets is a CCC 20 -- Sets is a CCC
21 21
22 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ 22 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
23 23
24 data One : Set c₁ where 24 c₂ = suc c₁
25 c₃ = suc c₂
26
27 data One {c : Level } : Set c where
25 OneObj : One -- () in Haskell ( or any one object set ) 28 OneObj : One -- () in Haskell ( or any one object set )
26 29
27 sets : CCC (Sets {c₁}) 30 sets : CCC (Sets {c₁})
28 sets = record { 31 sets = record {
29 １ = One 32 １ = One
93 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} → 96 *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} →
94 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] 97 Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
95 *-cong refl = refl 98 *-cong refl = refl
96 99
97 open import graph 100 open import graph
98 module ccc-from-graph (G : Graph {c₁} {c₁} ) where 101 module ccc-from-graph (G : Graph {c₂} {c₁} ) where
99 102
100 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) 103 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
101 open Graph 104 open Graph
102 105
103 data Objs : Set c₁ where 106 data Objs : Set c₂ where
104 atom : (vertex G) → Objs 107 atom : (vertex G) → Objs
105 ⊤ : Objs 108 ⊤ : Objs
106 _∧_ : Objs → Objs → Objs 109 _∧_ : Objs → Objs → Objs
107 _<=_ : Objs → Objs → Objs 110 _<=_ : Objs → Objs → Objs
108 111
109 data Arrows : (b c : Objs ) → Set c₁ 112 data Arrows : (b c : Objs ) → Set c₂
110 data Arrow : Objs → Objs → Set c₁ where --- case i 113 data Arrow : Objs → Objs → Set c₂ where --- case i
111 arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b) 114 arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b)
112 π : {a b : Objs } → Arrow ( a ∧ b ) a 115 π : {a b : Objs } → Arrow ( a ∧ b ) a
113 π' : {a b : Objs } → Arrow ( a ∧ b ) b 116 π' : {a b : Objs } → Arrow ( a ∧ b ) b
114 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a 117 ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
115 _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v 118 _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b ) --- case v
141 assoc≡ (○ a) g h = refl 144 assoc≡ (○ a) g h = refl
142 assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h) 145 assoc≡ < f , f₁ > g h = cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h)
143 assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) 146 assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h )
144 147
145 -- positive intutionistic calculus 148 -- positive intutionistic calculus
146 PL : Category c₁ c₁ c₁ 149 PL : Category c₂ c₂ c₂
147 PL = record { 150 PL = record {
148 Obj = Objs; 151 Obj = Objs;
149 Hom = λ a b → Arrows a b ; 152 Hom = λ a b → Arrows a b ;
150 _o_ = λ{a} {b} {c} x y → x ・ y ; 153 _o_ = λ{a} {b} {c} x y → x ・ y ;
151 _≈_ = λ x y → x ≡ y ; 154 _≈_ = λ x y → x ≡ y ;
173 C = graphtocat.Chain G 176 C = graphtocat.Chain G
174 177
175 tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b 178 tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
176 tr f x y = graphtocat.next f (x y) 179 tr f x y = graphtocat.next f (x y)
177 180
178 fobj : ( a : Objs ) → Set c₁ 181 fobj : ( a : Objs ) → Set c₂
179 fobj (atom x) = ( y : vertex G ) → C y x 182 fobj (atom x) = ( y : vertex G ) → C y x
180 fobj ⊤ = One 183 fobj ⊤ = One
181 fobj (a ∧ b) = ( fobj a /\ fobj b) 184 fobj (a ∧ b) = ( fobj a /\ fobj b)
182 fobj (a <= b) = fobj b → fobj a 185 fobj (a <= b) = fobj b → fobj a
183 186
196 -- CS is a map from Positive logic to Sets 199 -- CS is a map from Positive logic to Sets
197 -- Sets is CCC, so we have a cartesian closed category generated by a graph 200 -- Sets is CCC, so we have a cartesian closed category generated by a graph
198 -- as a sub category of Sets 201 -- as a sub category of Sets
199 202
200 CS : Functor PL (Sets {c₁}) 203 CS : Functor PL (Sets {c₁})
201 FObj CS a = fobj a 204 FObj CS a = {!!} -- fobj a
202 FMap CS {a} {b} f = fmap {a} {b} f 205 FMap CS {a} {b} f = {!!} -- fmap {a} {b} f
203 isFunctor CS = isf where 206 isFunctor CS = {!!} where -- isf where
204 _+_ = Category._o_ PL 207 _+_ = Category._o_ PL
205 ++idR = IsCategory.identityR ( Category.isCategory PL ) 208 ++idR = IsCategory.identityR ( Category.isCategory PL )
206 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) 209 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)
207 distr {a} {a₁} {a₁} {f} {id a₁} z = refl 210 distr {a} {a₁} {a₁} {f} {id a₁} z = refl
208 distr {a} {a₁} {⊤} {f} {○ a₁} z = refl 211 distr {a} {a₁} {⊤} {f} {○ a₁} z = refl
224 --- SM can be eliminated if we have 227 --- SM can be eliminated if we have
225 --- sobj (a : vertex g ) → {a} a set have only a 228 --- sobj (a : vertex g ) → {a} a set have only a
226 --- smap (a b : vertex g ) → {a} → {b} 229 --- smap (a b : vertex g ) → {a} → {b}
227 230
228 231
229 record CCCObj : Set (suc c₁) where 232 record CCCObj : Set c₃ where
230 field 233 field
231 cat : Category c₁ c₁ c₁ 234 cat : Category c₂ c₁ c₁
232 ≡←≈ : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g 235 ≡←≈ : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g
233 ccc : CCC cat 236 ccc : CCC cat
234 237
235 open CCCObj 238 open CCCObj
236 239
237 record CCCMap (A B : CCCObj ) : Set (suc c₁) where 240 record CCCMap (A B : CCCObj ) : Set c₃ where
238 field 241 field
239 cmap : Functor (cat A ) (cat B ) 242 cmap : Functor (cat A ) (cat B )
240 ccf : CCC (cat A) → CCC (cat B) 243 ccf : CCC (cat A) → CCC (cat B)
241 244
242 open import Category.Cat 245 open import Category.Cat
243 246
244 open CCCMap 247 open CCCMap
245 open import Relation.Binary.Core 248 open import Relation.Binary.Core
246 249
247 Cart : Category (suc c₁) (suc c₁) (suc c₁) 250 Cart : Category c₃ c₃ c₃
248 Cart = record { 251 Cart = record {
249 Obj = CCCObj 252 Obj = CCCObj
250 ; Hom = CCCMap 253 ; Hom = CCCMap
251 ; _o_ = λ {A} {B} {C} f g → record { cmap = (cmap f) ○ ( cmap g ) ; ccf = λ _ → ccf f ( ccf g (ccc A )) } 254 ; _o_ = λ {A} {B} {C} f g → record { cmap = (cmap f) ○ ( cmap g ) ; ccf = λ _ → ccf f ( ccf g (ccc A )) }
252 ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g 255 ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g
263 }} 266 }}
264 267
265 open import graph 268 open import graph
266 open Graph 269 open Graph
267 270
268 record GMap (x y : Graph {c₁} {c₁} ) : Set (suc c₁) where 271 record GMap (x y : Graph {c₂} {c₁} ) : Set c₂ where
269 field 272 field
270 vmap : vertex x → vertex y 273 vmap : vertex x → vertex y
271 emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b) 274 emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
272 275
273 open GMap 276 open GMap
274 277
275 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) 278 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )
276 279
277 data [_]_==_ (C : Graph {c₁} {c₁} ) {A B : vertex C} (f : edge C A B) 280 data [_]_==_ (C : Graph {c₂} {c₁} ) {A B : vertex C} (f : edge C A B)
278 : ∀{X Y : vertex C} → edge C X Y → Set (suc c₁) where 281 : ∀{X Y : vertex C} → edge C X Y → Set c₂ where
279 mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g 282 mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g
280 283
281 _=m=_ : {C D : Graph {c₁} {c₁} } 284 _=m=_ : {C D : Graph {c₂} {c₁} }
282 → (F G : GMap C D) → Set (suc c₁) 285 → (F G : GMap C D) → Set c₂
283 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f 286 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f
284 287
285 _&_ : {x y z : Graph {c₁} {c₁}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z 288 _&_ : {x y z : Graph {c₂} {c₁}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
286 f & g = record { vmap = λ x → vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) } 289 f & g = record { vmap = λ x → vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) }
287 290
288 Grph : Category (suc c₁) (suc c₁) (suc c₁) 291 Grph : Category c₃ c₂ c₂
289 Grph = record { 292 Grph = record {
290 Obj = Graph {c₁} {c₁} 293 Obj = Graph {c₂} {c₁}
291 ; Hom = GMap 294 ; Hom = GMap
292 ; _o_ = _&_ 295 ; _o_ = _&_
293 ; _≈_ = _=m=_ 296 ; _≈_ = _=m=_
294 ; Id = record { vmap = λ y → y ; emap = λ f → f } 297 ; Id = record { vmap = λ y → y ; emap = λ f → f }
295 ; isCategory = record { 298 ; isCategory = record {
297 ; identityL = λ e → mrefl refl 300 ; identityL = λ e → mrefl refl
298 ; identityR = λ e → mrefl refl 301 ; identityR = λ e → mrefl refl
299 ; o-resp-≈ = m--resp-≈ 302 ; o-resp-≈ = m--resp-≈
300 ; associative = λ e → mrefl refl 303 ; associative = λ e → mrefl refl
301 }} where 304 }} where
302 msym : {x y : Graph {c₁} {c₁} } { f g : GMap x y } → f =m= g → g =m= f 305 msym : {x y : Graph {c₂} {c₁} } { f g : GMap x y } → f =m= g → g =m= f
303 msym {x} {y} f=g f = lemma ( f=g f ) where 306 msym {x} {y} f=g f = lemma ( f=g f ) where
304 lemma : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f 307 lemma : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f
305 lemma (mrefl Ff≈Gf) = mrefl (sym Ff≈Gf) 308 lemma (mrefl Ff≈Gf) = mrefl (sym Ff≈Gf)
306 mtrans : {x y : Graph {c₁} {c₁} } { f g h : GMap x y } → f =m= g → g =m= h → f =m= h 309 mtrans : {x y : Graph {c₂} {c₁} } { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
307 mtrans {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where 310 mtrans {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where
308 lemma : ∀{a b c d e f} {p : edge y a b} {q : edge y c d} → {r : edge y e f} → [ y ] p == q → [ y ] q == r → [ y ] p == r 311 lemma : ∀{a b c d e f} {p : edge y a b} {q : edge y c d} → {r : edge y e f} → [ y ] p == q → [ y ] q == r → [ y ] p == r
309 lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv eqv₁ ) 312 lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv eqv₁ )
310 ise : {x y : Graph {c₁} {c₁}} → IsEquivalence {_} {suc c₁ } {_} ( _=m=_ {x} {y}) 313 ise : {x y : Graph {c₂} {c₁}} → IsEquivalence {_} {suc c₁ } {_} ( _=m=_ {x} {y})
311 ise = record { 314 ise = record {
312 refl = λ f → mrefl refl 315 refl = λ f → mrefl refl
313 ; sym = msym 316 ; sym = msym
314 ; trans = mtrans 317 ; trans = mtrans
315 } 318 }
316 m--resp-≈ : {A B C : Graph {c₁} {c₁} } 319 m--resp-≈ : {A B C : Graph {c₂} {c₁} }
317 {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g ) 320 {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g )
318 m--resp-≈ {A} {B} {C} {f} {g} {h} {i} f=g h=i e = 321 m--resp-≈ {A} {B} {C} {f} {g} {h} {i} f=g h=i e =
319 lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where 322 lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where
320 lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) → 323 lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) →
321 [ B ] ϕ == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π 324 [ B ] ϕ == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π
363 open ccc-from-graph.Objs 366 open ccc-from-graph.Objs
364 open ccc-from-graph.Arrow 367 open ccc-from-graph.Arrow
365 open ccc-from-graph.Arrows 368 open ccc-from-graph.Arrows
366 open graphtocat.Chain 369 open graphtocat.Chain
367 370
368 Sets0 : Category (suc c₁) c₁ c₁ 371 Sets0 : Category c₂ c₁ c₁
369 Sets0 = Sets {c₁} 372 Sets0 = Sets {c₁}
370 373
371 ccc-graph-univ : UniversalMapping Grph Cart forgetful.UX 374 ccc-graph-univ : UniversalMapping Grph Cart forgetful.UX
372 ccc-graph-univ = record { 375 ccc-graph-univ = record {
373 F = λ g → csc g ; 376 F = λ g → csc g ;
374 η = λ a → record { vmap = λ y → graphtocat.Chain {!!} {!!} {!!} ; emap = λ f x y → next f (x y) } ; -- graphtocat.Chain a ? ? 377 η = λ a → record { vmap = λ y → {!!} ; emap = λ f x → {!!} } ; -- graphtocat.Chain a ? ?
375 _* = solution ; 378 _* = solution ;
376 isUniversalMapping = record { 379 isUniversalMapping = record {
377 universalMapping = {!!} ; 380 universalMapping = {!!} ;
378 uniquness = {!!} 381 uniquness = {!!}
379 } 382 }
380 } where 383 } where
381 open forgetful 384 open forgetful
382 open ccc-from-graph 385 open ccc-from-graph
383 csc : Graph {c₁} {c₁} → Obj Cart 386 csc : Graph {c₂} {c₁} → Obj Cart
384 csc g = record { cat = {!!} ; ccc = {!!} ; ≡←≈ = λ eq → eq } 387 csc g = record { cat = Sets ; ccc = sets ; ≡←≈ = λ eq → eq }
385 cs : (g : Graph {c₁}{c₁} ) → Functor (ccc-from-graph.PL g) (Sets {suc c₁}) 388 cs : (g : Graph {c₂}{c₁} ) → Functor (ccc-from-graph.PL g) (Sets {c₁})
386 cs g = {!!} 389 cs g = CS g
387 pl : (g : Graph {c₁} {c₁ } ) → Category _ _ _ 390 pl : (g : Graph {c₂} {c₁ } ) → Category _ _ _
388 pl g = PL g 391 pl g = PL g
389 cobj : {g : Obj (Grph )} {c : Obj (Cart)} → Hom Grph g (FObj UX c) → Objs {!!} → Obj (cat c) 392 cobj : {g : Obj Grph } {c : Obj Cart} → Hom Grph g (FObj UX c) → Objs g → Obj (cat c)
390 cobj {g} {c} f (atom x) = vmap f {!!} 393 cobj {g} {c} f (atom x) = vmap f x
391 cobj {g} {c} f ⊤ = CCC.１ (ccc c) 394 cobj {g} {c} f ⊤ = CCC.１ (ccc c)
392 cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y) 395 cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y)
393 cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) 396 cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a)
394 c-map : {g : Obj (Grph )} {c : Obj Cart} {A B : Objs {!!}} 397 c-map : {g : Obj (Grph )} {c : Obj Cart} {A B : Objs {!!}}
395 → (f : Hom Grph g (FObj UX c) ) → (p : Hom (pl {!!}) A B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B) 398 → (f : Hom Grph g (FObj UX c) ) → (p : Hom (pl {!!}) A B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
398 c-map {g} {c} {a ∧ b} {atom x} f (iv f1 y) = {!!} 401 c-map {g} {c} {a ∧ b} {atom x} f (iv f1 y) = {!!}
399 c-map {g} {c} {b <= a} {atom x} f y = {!!} 402 c-map {g} {c} {b <= a} {atom x} f y = {!!}
400 c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a) 403 c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
401 c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f {!!}) (c-map f {!!}) 404 c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f {!!}) (c-map f {!!})
402 c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f {!!}) 405 c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f {!!})
403 solution : {g : Obj (Grph )} {c : Obj (Cart )} → Hom Grph g (FObj UX c) → Hom (Cart ) {!!} {!!} 406 solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart {!!} {!!}
404 solution {g} {c} f = {!!} -- record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} } 407 solution {g} {c} f = {!!} -- record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }
405 408
406 409