Mercurial > hg > Members > kono > Proof > category

changeset 915:fa302d99fa40

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 09:30:44 +0900
parents 8c2da34e8dc1
children a79b08e12447
files CCCGraph.agda
diffstat 1 files changed, 7 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sat May 02 05:32:42 2020 +0900
+++ b/CCCGraph.agda	Sat May 02 09:30:44 2020 +0900
@@ -420,10 +420,15 @@
        cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) 
        c-map : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} {A B : Obj (cat (csc g))}
            → (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)
-       c-map {g} {c} {a} {atom x} f y = ?
+       c-map {g} {c} {atom a} {atom b} f y with y (λ w → {!!} ) a
+       c-map {g} {c} {atom a} {atom a} f y | id a = id1 (cat c) (cobj {g} {c} f (atom a))
+       c-map {g} {c} {atom a} {atom b} f y | next {a} {d} {b} x t = (cat c) [ emap f x o {!!} ] 
+       c-map {g} {c} {⊤} {atom x} f y = {!!}
+       c-map {g} {c} {a ∧ b} {atom x} f y = {!!}
+       c-map {g} {c} {b <= a} {atom x} f y = {!!}
        c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
        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)))
-       c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) {!!}  -- with c-map f x
+       c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f (λ w → (x (proj₁ w) (proj₂ w)) ))
        solution : {g : Obj Grph} {c : Obj Cart} → Hom Grph g (FObj UX c) → Hom Cart (csc g) c
        solution {g} {c} f = record { cmap = record { FObj = λ x → cobj {g} {c} f x ; FMap = c-map {g} {c} f ; isFunctor = {!!} } ; ccf = {!!} }