Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph.agda @ 942:5084433e0726

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 Sun, 17 May 2020 11:55:30 +0900
parents d26f21112e1c
children 3f2525c2b999
comparison
equal deleted inserted replaced
941:d26f21112e1c 942:5084433e0726
362 postulate 362 postulate
363 g21 : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} → Graph {c₁} {c₂} 363 g21 : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} → Graph {c₁} {c₂}
364 m21 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) → GMap {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁} {c₂} g (g21 g) 364 m21 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) → GMap {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁} {c₂} g (g21 g)
365 m12 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) → GMap {c₁} {c₂} {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} (g21 g) g 365 m12 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} ) → GMap {c₁} {c₂} {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} (g21 g) g
366 giso→ : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} } 366 giso→ : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} }
367 → {a b : vertex g } → {e : edge g a b } → (m12 g & m21 g) =m= id1 Grph g 367 → {a b : vertex g } → (m12 g & m21 g) =m= id1 Grph g
368 giso← : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} } 368 giso← : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} }
369 → {a b : vertex (g21 g) } → {e : edge (g21 g) a b } → (m21 g & m12 g ) =m= id1 Grph (g21 g) 369 → {a b : vertex (g21 g) } → (m21 g & m12 g ) =m= id1 Grph (g21 g)
370 -- Grph [ Grph [ m21 g o m12 g ] ≈ id1 Grph (g21 g) ] 370 -- Grph [ Grph [ m21 g o m12 g ] ≈ id1 Grph (g21 g) ]
371 371
372 fobj : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) → Obj Grph 372 fobj : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) → Obj Grph
373 fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) } 373 fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
374 fmap : {a b : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂} ) } → Hom (Cart ) a b → Hom (Grph {c₁} {c₂}) (g21 ( fobj a )) (g21 ( fobj b )) 374 fmap : {a b : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂} ) } → Hom (Cart ) a b → Hom (Grph {c₁} {c₂}) (g21 ( fobj a )) (g21 ( fobj b ))
379 UX : Functor (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {c₁} {c₂}) 379 UX : Functor (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {c₁} {c₂})
380 FObj UX a = g21 (fobj a) 380 FObj UX a = g21 (fobj a)
381 FMap UX f = fmap f 381 FMap UX f = fmap f
382 isFunctor UX = isf where 382 isFunctor UX = isf where
383 isf : IsFunctor Cart Grph (λ z → g21 (fobj z)) fmap 383 isf : IsFunctor Cart Grph (λ z → g21 (fobj z)) fmap
384 eff : (a : Obj Cart) (f : vertex (g21 (fobj a)) ) → edge (g21 (fobj a)) f f
385 eff a f = {!!}
386 IsFunctor.identity isf {a} {b} {f} = begin 384 IsFunctor.identity isf {a} {b} {f} = begin
387 fmap (id1 Cart a) 385 fmap (id1 Cart a)
388 ≈⟨⟩ 386 ≈⟨⟩
389 fmap {a} {a} (record { cmap = identityFunctor ; ccf = λ x → x }) 387 fmap {a} {a} (record { cmap = identityFunctor ; ccf = λ x → x })
390 ≈⟨⟩ 388 ≈⟨⟩
391 record { vmap = λ e → vmap (m21 (fobj a)) (vmap (m12 (fobj a)) e ) ; emap = λ e → emap (m21 (fobj a)) (emap (m12 (fobj a)) e )} 389 record { vmap = λ e → vmap (m21 (fobj a)) (vmap (m12 (fobj a)) e ) ; emap = λ e → emap (m21 (fobj a)) (emap (m12 (fobj a)) e )}
392 ≈⟨ giso← {fobj a} {f} {f} {eff a f } ⟩ 390 ≈⟨ giso← {fobj a} {f} {f} ⟩
393 record { vmap = λ y → y ; emap = λ f → f } 391 record { vmap = λ y → y ; emap = λ f → f }
394 ≈⟨⟩ 392 ≈⟨⟩
395 id1 Grph (g21 (fobj a)) 393 id1 Grph (g21 (fobj a))
396 ∎ where open ≈-Reasoning Grph 394 ∎ where open ≈-Reasoning Grph
397 IsFunctor.distr isf {a} {b} {c} {f} {g} = begin 395 IsFunctor.distr isf {a} {b} {c} {f} {g} = begin
398 fmap ( Cart [ g o f ] ) 396 fmap ( Cart [ g o f ] )
399 ≈⟨⟩ 397 ≈⟨⟩
400 record { vmap = λ e → vmap (m21 (fobj c)) (FObj (cmap (Cart [ g o f ] )) (vmap (m12 (fobj a)) e)) ; 398 ( m21 (fobj c) & ( record { vmap = λ e → FObj (cmap (( Cart [ g o f ] ))) e ; emap = λ e → FMap (cmap (( Cart [ g o f ] ))) e} & m12 (fobj a) ) )
401 emap = λ e → emap (m21 (fobj c)) (FMap (cmap (Cart [ g o f ] )) (emap (m12 (fobj a)) e)) }
402 ≈⟨ {!!} ⟩ 399 ≈⟨ {!!} ⟩
403 record { vmap = λ e → vmap (m21 (fobj c)) (FObj (cmap g) (vmap (m12 (fobj b)) (vmap (fmap f) e))); 400 ( m21 (fobj c) & (record { vmap = λ e → FObj (cmap g) (FObj (cmap f) e) ; emap = λ e → FMap (cmap g) (FMap (cmap f) e) }
404 emap = λ e → emap (m21 (fobj c)) (FMap (cmap g) (emap (m12 (fobj b)) (emap (fmap f) e))) } 401 & m12 (fobj a)))
402 ≈⟨ cdr (cdr (car (giso← {fobj b} ))) ⟩
403 ( m21 (fobj c) & (record { vmap = λ e → FObj (cmap g) e ; emap = λ e → FMap (cmap g) e}
404 & ((m12 (fobj b)
405 & (m21 (fobj b))) & (record { vmap = λ e → FObj (cmap f) e ; emap = λ e → FMap (cmap f) e}
406 & (m12 (fobj a) )))))
405 ≈⟨⟩ 407 ≈⟨⟩
406 Grph [ fmap g o fmap f ] 408 Grph [ fmap g o fmap f ]
407 ∎ where open ≈-Reasoning Grph 409 ∎ where open ≈-Reasoning Grph
408 IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = {!!} where -- lemma ( (extensionality Sets ( λ z → lemma4 ( 410 IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = {!!} where -- lemma ( (extensionality Sets ( λ z → lemma4 (
409 -- ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g))) 411 -- ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
444 -- | | 446 -- | |
445 -- | Functor (CS g) | 447 -- | Functor (CS g) |
446 -- ↓ | 448 -- ↓ |
447 -- Sets ((z : vertx g) → C z x) ----> ((z : vertx g) → C z y) = h : Hom Sets (fobj (atom x)) (fobj (atom y)) 449 -- Sets ((z : vertx g) → C z x) ----> ((z : vertx g) → C z y) = h : Hom Sets (fobj (atom x)) (fobj (atom y))
448 -- 450 --
449 cs : {c₁ c₂ : Level} → (g : Graph {c₁} {c₂} ) → Functor (ccc-from-graph.PL g) (Sets {_})
450 cs g = CS g
451 F : Obj (Grph {c₁} {c₂}) → Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) 451 F : Obj (Grph {c₁} {c₂}) → Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
452 F g = record { cat = Sets {c₁ ⊔ c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } 452 F g = record { cat = Sets {c₁ ⊔ c₂} ; ccc = sets ; ≡←≈ = λ eq → eq }
453 η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a)) 453 η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a))
454 η a = record { vmap = λ y → vm y ; emap = λ f → em f } where 454 η a = record { vmap = λ y → vm y ; emap = λ f → em f } where
455 fo : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} 455 fo : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}
482 identity = {!!} ; 482 identity = {!!} ;
483 distr = {!!} ; 483 distr = {!!} ;
484 ≈-cong = {!!} 484 ≈-cong = {!!}
485 } 485 }
486 } 486 }
487 submap : (g : Graph {c₁} {c₂}) → Functor (Sets {c₁ ⊔ c₂} )(Sets {c₁ ⊔ c₂} )
488 submap g = record {
489 FObj = λ x → Objs {!!} ;
490 FMap = λ {x} {y} h → {!!} ;
491 isFunctor = {!!}
492 }
487 solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (F g) c 493 solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (F g) c
488 solution {g} {c} f = record { cmap = record { 494 solution {g} {c} f = record { cmap = record {
489 FObj = λ x → cobj {g} {c} f (xtog x ) ; 495 FObj = λ x → cobj {g} {c} f (xtog x ) ;
490 FMap = λ {x} {y} h → c-map {g} {c} f (htop {x} {y} h ) ; 496 FMap = λ {x} {y} h → c-map {g} {c} f (htop {x} {y} h ) ;
491 isFunctor = {!!} } ; 497 isFunctor = {!!} } ;