Mercurial > hg > Members > kono > Proof > category

changeset 921:625baac95ec8

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 15:45:20 +0900
parents c10ee19a1ea3
children 348ed0c473cc 5eed22f4a75d
files CCCGraph.agda
diffstat 1 files changed, 11 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Mon May 04 14:34:42 2020 +0900
+++ b/CCCGraph.agda	Mon May 04 15:45:20 2020 +0900
@@ -252,17 +252,21 @@
                     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))
+   data plcase {b : vertex G}  : {a : Objs } → (f : Hom PL a (atom b)) → ( sf : Hom CSC a (atom b)) → Set (c₁ ⊔ c₂) where
+       pid :  plcase (id (atom b)) (id1 CSC (atom b))
+       parrow : {a : Objs } {c : vertex G} → (x : edge G c b) → (f : Arrows a (atom c))
            → 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))
+       pπ : {a c : Objs } (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) ))
+       pπ' : {a c : Objs } (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))
+       pε : {a c : Objs } (f : Arrows a ((atom b <= c) ∧ c))
            → plcase (iv ε f) (λ y → proj₁ (fmap f y ) (proj₂ (fmap f y )) )
 
+   rev : {a : Objs } → {b : vertex G}  → ( sf : Hom CSC a (atom b)) → {f : Hom PL a (atom b)} →  Hom PL a (atom b) 
+   rev {a} {b} sf {f} with plcase f sf
+   ... | t = {!!}
+
 
 ---
 ---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap 
@@ -430,8 +434,7 @@
        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 with ccc-from-graph.plcase g ? y
-       ... | t = {!!}
+       c-map {g} {c} {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) ( c-map f (λ w → x (proj₁ w) (proj₂ w)))