Mercurial > hg > Members > kono > Proof > category

comparison CCCGraph.agda @ 914:8c2da34e8dc1

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 Sat, 02 May 2020 05:32:42 +0900
parents 635418b4b2f3
children fa302d99fa40 c10ee19a1ea3
comparison
equal deleted inserted replaced
913:c5446790ddb1 914:8c2da34e8dc1
412 } where 412 } where
413 csc : Graph → Obj Cart 413 csc : Graph → Obj Cart
414 csc g = record { cat = CSC ; ccc = cc1 ; ≡←≈ = λ eq → eq } where 414 csc g = record { cat = CSC ; ccc = cc1 ; ≡←≈ = λ eq → eq } where
415 open ccc-from-graph g 415 open ccc-from-graph g
416 cobj : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} → Hom Grph g (FObj UX c) → Obj (cat (csc g)) → Obj (cat c) 416 cobj : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} → Hom Grph g (FObj UX c) → Obj (cat (csc g)) → Obj (cat c)
417 cobj {g} {c} f (atom x) = {!!} 417 cobj {g} {c} f (atom x) = vmap f x
418 cobj {g} {c} f ⊤ = CCC.１ (ccc c) 418 cobj {g} {c} f ⊤ = CCC.１ (ccc c)
419 cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) {!!} {!!} 419 cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y)
420 cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) {!!} {!!} 420 cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a)
421 c-map : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} {A B : Obj (cat (csc g))}
422 → (f : Hom Grph g (FObj UX c) ) → Hom (cat (csc g)) A B → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
423 c-map {g} {c} {a} {atom x} f y = ?
424 c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
425 c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f (λ w → proj₁ (z w))) (c-map f (λ w → proj₂ (z w)))
426 c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) {!!} -- with c-map f x
421 solution : {g : Obj Grph} {c : Obj Cart} → Hom Grph g (FObj UX c) → Hom Cart (csc g) c 427 solution : {g : Obj Grph} {c : Obj Cart} → Hom Grph g (FObj UX c) → Hom Cart (csc g) c
422 solution {g} {c} f = record { cmap = record { FObj = λ x → cobj {g} {c} f x ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} } 428 solution {g} {c} f = record { cmap = record { FObj = λ x → cobj {g} {c} f x ; FMap = c-map {g} {c} f ; isFunctor = {!!} } ; ccf = {!!} }
423 429
424 430