Mercurial > hg > Members > kono > Proof > category

changeset 923:8380d1af9890

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 Mon, 04 May 2020 20:46:17 +0900
parents 348ed0c473cc
children 45535a053f42
files CCCGraph.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!}