Mercurial > hg > Members > kono > Proof > category

changeset 946:f8e6e9128f3d

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, 18 May 2020 18:41:55 +0900
parents 94ece478b583
children 095fd0829ccf
files CCCGraph.agda
diffstat 1 files changed, 24 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sun May 17 23:07:18 2020 +0900
+++ b/CCCGraph.agda	Mon May 18 18:41:55 2020 +0900
@@ -428,6 +428,25 @@
 
   open ccc-from-graph g
 
+  FCat' : Obj (Cart {suc c₁} {suc c₁ ⊔ c₂} {c₁ ⊔ c₂})
+  FCat'  = record { cat = record {
+          Obj = Obj PL 
+          ; Hom = λ a b → {f : Hom PL a b } → Hom B (FObj CS a) (FObj CS b)
+          ; _o_ = {!!}
+          ; _≈_ = {!!}
+          ; Id  = λ {a} → id1 B (FObj CS a)
+          ; isCategory = record {
+                    isEquivalence =  {!!};
+                    identityL  = λ {a b f} → {!!};
+                    identityR  = λ {a b f} → {!!};
+                    o-resp-≈  = λ {a b c f g h i} → {!!};
+                    associative  = λ{a b c d f g h } → {!!} } 
+          } ; 
+         ≡←≈  = λ eq → {!!} ;
+         ccc = {!!}
+      } where
+          B = Sets {c₁ ⊔ c₂}
+
   FCat : Obj (Cart {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
   FCat  = record { cat = record {
           Obj = Obj PL 
@@ -474,7 +493,7 @@
        --  Sets  ((z : vertx g) → C z x)  ----> ((z : vertx g) → C z y)  = h : Hom Sets (fobj (atom x)) (fobj (atom y))
        --
        F : Obj (Grph {c₁} {c₂}) → Obj (Cart {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
-       F g = FCat  where open fcat g -- record { cat = Sets  {c₁ ⊔ c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } 
+       F g = FCat'  where open fcat g 
        η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a))
        η a = record { vmap = λ y → vm y ;  emap = λ f → em f }  where
             fo : Graph  {suc c₁ } {c₁ ⊔ c₂}
@@ -492,13 +511,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} {A B : Objs g} 
            → (f : Hom Grph g (FObj UX c) ) → (fobj g A → fobj g B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
-       c-map {g} {c} {atom a} {atom x} f y = {!!}
-       c-map {g} {c} {⊤} {atom x} f y = ?
-       c-map {g} {c} {a ∧ b} {atom x} f y = {!!}
-       c-map {g} {c} {b <= a} {atom x} f y = {!!}
+       c-map {g} {c} {a} {atom b} f y = {!!} 
+       -- with emap (m12 (uobj {c₁} {c₂} c)) ( emap f {!!} )
        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 {!!}) (c-map f {!!})
-       c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f {!!})
+       c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f (λ k → proj₁ (z k))) (c-map f (λ k → proj₂ (z k)))
+       c-map {g} {c} {d} {b <= a} f x = CCC._* (ccc c) ( c-map f (λ k → x (proj₁ k)  (proj₂ k)))
        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 →  cobj {g} {c} f x ;