Mercurial > hg > Members > kono > Proof > category

changeset 993:194d4ad4efd9

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 Sat, 06 Mar 2021 16:50:47 +0900
parents c1576827404e
children 485bc7560a75
files src/CCCGraph.agda
diffstat 1 files changed, 26 insertions(+), 29 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCGraph.agda	Sat Mar 06 13:35:45 2021 +0900
+++ b/src/CCCGraph.agda	Sat Mar 06 16:50:47 2021 +0900
@@ -96,17 +96,16 @@
                 *-cong refl = refl
 
 
-tooos : {c : Level } → Topos (Sets {c}) sets
-tooos  = record {
-         Ω = {!!}
-      ;  ⊤ = {!!}
-      ;  Ker = {!!}
-      ;  char = {!!}
-      ;  isTopos = record {
- 
-         }
-    }
-
+-- tooos : {c : Level } → Topos (Sets {c}) sets
+-- tooos  = record {
+--          Ω = {!!}
+--       ;  ⊤ = {!!}
+--       ;  Ker = {!!}
+--       ;  char = {!!}
+--       ;  isTopos = record {
+--  
+--          }
+--     }
 
 
 open import graph
@@ -447,7 +446,7 @@
                     identityL  = λ {a b f} → IsCategory.identityL (Category.isCategory B) ;
                     identityR  = λ {a b f} → IsCategory.identityR (Category.isCategory B) ;
                     o-resp-≈  = λ {a b c f g h i} → IsCategory.o-resp-≈ (Category.isCategory B);
-                    associative  = λ {a} {b} {c} {f} {g} {h} → ? -- IsCategory.associative (Category.isCategory B) {{!!}} {{!!}} {{!!}} {{!!}} {{!!}} {{!!}}
+                    associative  = λ {a} {b} {c} {f} {g} {h} → {!!} -- IsCategory.associative (Category.isCategory B) {{!!}} {{!!}} {{!!}} {{!!}} {{!!}} {{!!}}
              }
           } ;
          ≡←≈  = λ eq → eq ;
@@ -476,7 +475,7 @@
        -- 
        -- 
        --                                        η : Hom Grph a (FObj UX (F a))
-       --                    f : edge g x y   ----------------------------------->  m21 (record {vertex = fobj (atom x) ; edge = fmap h }) : Graph
+       --                    f : edge g x y   ----------------------------------->  (record {vertex = fobj (atom x) ; edge = fmap h }) : Graph
        --  Graph g     x  ----------------------> y : vertex g                             ↑
        --                       arrow f             : Hom (PL g) (atom x) (atom y)         |
        --  PL g     atom x  ------------------> atom y : Obj (PL g)                        | UX : Functor Sets Graph
@@ -488,30 +487,28 @@
        F : Obj (Grph {c₁} {c₁}) → Obj (Cart {c₁} {c₁} {c₁})
        F g = FCat  where open fcat g 
        η : (a : Obj (Grph {c₁} {c₁}) ) → Hom Grph a (FObj UX (F a))
-       η a = record { vmap = λ y → {!!} ;  emap = λ f → em f }  where
+       η a = record { vmap = λ y → vm y ;  emap = λ f → em f }  where
             fo : Graph  {c₁ } {c₁}
             fo = uobj {c₁} (F a)
-            vm : (y : vertex a ) →  vertex {!!}
-            vm y =  {!!} -- vmap (m21 fo) (atom y) 
-            em :  { x y : vertex a } (f : edge a x y ) → edge (FObj UX (F a)) {!!} {!!}
-            em {x} {y} f = {!!} -- emap (m21 fo) (fmap a (iv (arrow f) (id _)))
-       pl : {c₁ c₁ : Level}  → (g : Graph {c₁} {c₁} ) → Category _ _ _
-       pl g = PL g
+            vm : (y : vertex a ) →  vertex (FObj UX (F a))
+            vm y =  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 = fmap a (iv (arrow f) (id _))
        cobj  :  {g : Obj (Grph {c₁} {c₁} ) } {c : Obj Cart} → Hom Grph g (FObj UX c)  → Objs g → Obj (cat c)
-       cobj {g} {c} f (atom x) = vmap {!!} (vmap f x)
+       cobj {g} {c} f (atom x) = vmap f x 
        cobj {g} {c} f ⊤ = CCC.１ (ccc c)
        cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y)
        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} {a} {atom b} f y with fcat.fcat-pl {c₁} {c₁} g {a} {atom b} y
-       c-map {g} {c} {atom b} {atom b} f y | id (atom b) = id1 (cat c) _
-       c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} (arrow x) t = {!!} 
-          -- (cat c) [ emap (m12 (uobj {c₁} {c₁} c)) ( emap f x)  o c-map {g} {c} {a} {d} f (fmap g t) ]
-       c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} π t = {!!} --(cat c) [ CCC.π (ccc c) o c-map {g} {c} {a} {d} f (fmap g t)]
-       c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} π' t = {!!} -- (cat c) [ CCC.π' (ccc c) o c-map {g} {c} {a} {d} f (fmap g t) ]
-       c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} ε t = {!!} -- (cat c) [ CCC.ε (ccc c) o c-map {g} {c} {a} {d} f (fmap g t) ]
-       -- with emap (m12 (uobj {c₁} {c₁} c)) ( emap f {!!} )
+       --- Hom (cat c) (cobj f a) (cobj f (atom b))
+      ------ g  : Obj Grph
+      ------ c  : Obj Cart
+      ------ a  : Objs g
+      ------ b  : V g
+      ------ f  : Hom Grph g (uobj c)
+      ------ y  : fobj g a → (y₁ : vertex g) → C g y₁ b
+       c-map {g} {c} {a} {atom b} 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 (λ 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)))