# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1588592777 -32400
# Node ID 8380d1af9890aac40604b5ea61355f0308f59499
# Parent  348ed0c473ccd11b52e22bce982d662ef4f33a13
...

diff -r 348ed0c473cc -r 8380d1af9890 CCCGraph.agda
--- a/CCCGraph.agda	Mon May 04 18:54:24 2020 +0900
+++ b/CCCGraph.agda	Mon May 04 20:46:17 2020 +0900
@@ -450,8 +450,8 @@
        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 with proof y
-       c-map {g} {c} {atom x} {atom x} f y | id (atom x) = {!!}
-       c-map {g} {c} {a} {atom x} f y | iv {_} {_} {atom d} (arrow z) t with (func y) ?  d
+       c-map {g} {c} {atom x} {atom x} f y | id (atom x) = id1 (cat c) (cobj {g} {c} f (atom x))
+       c-map {g} {c} {a} {atom x} f y | iv {_} {_} {atom d} (arrow z) t with (func y) {!!}  d
        ... | t11 = {!!}
        c-map {g} {c} {a} {atom x} f y | iv π t = {!!} -- c-map f ( record { func = λ z → proj₁ ? ; proof = t } ) 
        c-map {g} {c} {a} {atom x} f y | iv π' t = {!!}