Mercurial > hg > Members > kono > Proof > category

changeset 937:2385fdd6818b

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 Fri, 15 May 2020 20:43:42 +0900
parents d13e0981e667
children 24248f9249c5
files CCCGraph.agda
diffstat 1 files changed, 14 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Fri May 15 20:10:09 2020 +0900
+++ b/CCCGraph.agda	Fri May 15 20:43:42 2020 +0900
@@ -415,6 +415,9 @@
   } where
        open forgetful  
        open ccc-from-graph
+       -- 
+       --  In our scheme, CAT/Cart/Grph does not allow different levels of objects, so we assume level conversion on Graph
+       -- 
        --                                        η : Hom Grph a (FObj UX (F a))
        --                    f : edge g x y   ----------------------------------->  m21 (record {vertex = fobj (atom x) ; edge = fmap h }) : Graph
        --  Graph g     x  ----------------------> y : vertex g                             ↑
@@ -437,11 +440,6 @@
             vm y =  vmap (m21 fo) (ccc-from-graph.fobj a (atom y))
             em :  { x y : vertex a } (f : edge a x y ) → edge (FObj UX (F a)) (vm x) (vm y)
             em {x} {y} f = emap (m21 fo) (ccc-from-graph.fmap a (iv (arrow f) (id _)))
-            
-       --    k : ( y : vertex a) → Set (c₁ ⊔ c₂)
-       --    k y = ( e : vertex a ) → graphtocat.Chain a e y
-       --    mm : Graph {suc (c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}
-       --    mm = forgetful.fobj {c₁} {c₂} (F a)
        pl : {c₁ c₂ : Level}  → (g : Graph {c₁} {c₂} ) → Category _ _ _
        pl g = PL g
        cobj  :  {g : Obj (Grph {c₁} {c₂} ) } {c : Obj Cart} → Hom Grph g (FObj UX c)  → Objs g → Obj (cat c)
@@ -459,6 +457,15 @@
        c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f {!!}) (c-map f {!!})
        c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f {!!})
        solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (F g) c
-       solution  {g} {c} f = {!!} -- record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }
+       solution  {g} {c} f = record { cmap = record {
+             FObj = λ x → cobj {g} {c} f (xtog x) ;
+             FMap = λ {x} {y} h → c-map {g} {c} f (htop {x} {y} h )  ;
+             isFunctor = {!!} } ;
+             ccf = {!!} } where
+                xtog : Obj Sets → Objs g
+                xtog x = {!!}
+                htop : {x y : Set (c₁ ⊔ c₂) } → (x → y) →  Hom (pl g) {!!} {!!}
+                htop = {!!}
+                fo : Graph  {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂}
+                fo = forgetful.fobj {c₁} {c₂} c
 
-