Mercurial > hg > Members > kono > Proof > category

changeset 920:c10ee19a1ea3

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 14:34:42 +0900
parents 8c2da34e8dc1
children 625baac95ec8
files CCCGraph.agda
diffstat 1 files changed, 13 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sat May 02 05:32:42 2020 +0900
+++ b/CCCGraph.agda	Mon May 04 14:34:42 2020 +0900
@@ -252,6 +252,16 @@
                     Sets [ f ≈ f' ] → Sets [  (λ x y → f (x , y)) ≈ (λ x y → f' (x , y)) ]
         *-cong refl = refl
 
+   data plcase : {a : Objs } → {b : vertex G}  → (f : Hom PL a (atom b)) → ( sf : Hom CSC a (atom b)) → Set (c₁ ⊔ c₂) where
+       pid : {b : vertex G} → plcase (id (atom b)) (id1 CSC (atom b))
+       parrow : {a : Objs } {b c : vertex G} → (x : edge G b c) → (f : Arrows a (atom b))
+           → plcase (iv (arrow x) f) ( λ y z → graphtocat.next x (fmap f y z )) 
+       pπ : {a c : Objs } {b : vertex G} → (f : Arrows a ((atom b) ∧ c))
+           → plcase (iv π f) (λ y → proj₁ (fmap f y ))
+       pπ' : {a c : Objs } {b : vertex G} → (f : Arrows a (c ∧ (atom b) ))
+           → plcase (iv π' f) (λ y → proj₂ (fmap f y ))
+       pε : {a c : Objs } {b : vertex G} → (f : Arrows a ((atom b <= c) ∧ c))
+           → plcase (iv ε f) (λ y → proj₁ (fmap f y ) (proj₂ (fmap f y )) )
 
 
 ---
@@ -420,10 +430,11 @@
        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} {a} {atom x} f y with ccc-from-graph.plcase g ? y
+       ... | t = {!!}
        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 = {!!} }