Mercurial > hg > Members > kono > Proof > category

changeset 944:c58684b15d97

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 Sun, 17 May 2020 18:42:17 +0900
parents 3f2525c2b999
children 94ece478b583
files CCCGraph.agda
diffstat 1 files changed, 39 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sun May 17 12:35:49 2020 +0900
+++ b/CCCGraph.agda	Sun May 17 18:42:17 2020 +0900
@@ -360,23 +360,23 @@
   -- Grph does not allow morph on different level graphs
   -- simply assumes we have iso to the another level. This may means same axiom on CCCs results the same CCCs.
   postulate
-     g21 : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} → Graph {c₁} {c₂} 
-     m21 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} )  → GMap  {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁} {c₂} g (g21 g)
-     m12 : (g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} )  → GMap  {c₁} {c₂}  {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} (g21 g) g
-     giso→  : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} }
+     g21 : Graph {suc c₁} {c₁ ⊔ c₂} → Graph {c₁} {c₂} 
+     m21 : (g : Graph {suc c₁ } {c₁ ⊔ c₂} )  → GMap  {suc c₁ } {c₁ ⊔ c₂} {c₁} {c₂} g (g21 g)
+     m12 : (g : Graph {suc c₁ } {c₁ ⊔ c₂} )  → GMap  {c₁} {c₂}  {suc c₁ } {c₁ ⊔ c₂} (g21 g) g
+     giso→  : { g : Graph {suc c₁ } {c₁ ⊔ c₂} }
           → {a b : vertex g } →  (m12 g & m21 g) =m= id1 Grph g
-     giso←  : { g : Graph {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} }
+     giso←  : { g : Graph {suc c₁ } {c₁ ⊔ c₂} }
           → {a b : vertex (g21 g) } →  (m21 g & m12 g ) =m= id1 Grph (g21 g)
                 -- Grph [ Grph [ m21 g o m12 g ] ≈ id1 Grph (g21 g) ]
   
-  fobj : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) → Obj Grph
+  fobj : Obj (Cart {suc c₁ } {c₁ ⊔ c₂} {c₁ ⊔ c₂}) → Obj Grph
   fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
-  fmap :  {a b : Obj (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂} ) } → Hom (Cart ) a b → Hom (Grph {c₁} {c₂}) (g21 ( fobj a )) (g21 ( fobj b ))
+  fmap :  {a b : Obj (Cart {suc c₁ } {c₁ ⊔ c₂} {c₁ ⊔ c₂} ) } → Hom (Cart ) a b → Hom (Grph {c₁} {c₂}) (g21 ( fobj a )) (g21 ( fobj b ))
   fmap {a} {b} f =  record {
            vmap = λ e → vmap (m21 (fobj b)) (FObj (cmap f) (vmap (m12 (fobj a)) e ))
          ; emap = λ e → emap (m21 (fobj b)) (FMap (cmap f) (emap (m12 (fobj a)) e )) } 
 
-  UX :  Functor (Cart  {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {c₁} {c₂})
+  UX :  Functor (Cart  {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {c₁} {c₂})
   FObj UX a = g21 (fobj a)
   FMap UX f =  fmap f
   isFunctor UX  = isf where
@@ -424,7 +424,32 @@
 Sets0 : {c₂ : Level } → Category (suc c₂) c₂ c₂
 Sets0 {c₂} = Sets {c₂}
 
-ccc-graph-univ :  {c₁ c₂ : Level} → UniversalMapping (Grph {c₁} {c₂}) (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) forgetful.UX 
+module fcat {c₁ c₂ : Level}  ( g : Graph {c₁} {c₂} ) where
+
+  open ccc-from-graph g
+
+  FCat : Obj (Cart {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
+  FCat  = record { cat = record {
+          Obj = Obj PL 
+          ; Hom = λ a b → fobj a → fobj b
+          ; _o_ = Category._o_ B
+          ; _≈_ = Category._≈_ B
+          ; Id  = λ {a} → id1 B (FObj CS a)
+          ; isCategory = record {
+                    isEquivalence =  IsCategory.isEquivalence (Category.isCategory B) ;
+                    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 d f g h } → IsCategory.associative (Category.isCategory B) 
+             }
+          } ;
+         ≡←≈  = λ eq → eq ;
+         ccc = {!!}
+      } where
+          B = Sets {c₁ ⊔ c₂}
+
+
+ccc-graph-univ :  {c₁ c₂ : Level} → UniversalMapping (Grph {c₁} {c₂}) (Cart {suc c₁ } {c₁ ⊔ c₂} {c₁ ⊔ c₂}) forgetful.UX 
 ccc-graph-univ {c₁} {c₂} = record {
      F = F ;
      η = η ; -- λ a → record { vmap = λ y →  graphtocat.Chain {!!} {!!} {!!}  ; emap = λ f x →  {!!} } ; -- 
@@ -448,25 +473,21 @@
        --                          ↓                                                       |
        --  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₁ ⊔ c₂})
-       F g = record { cat = Sets  {c₁ ⊔ c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } 
+       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 } 
        η : (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₁ ⊔ c₂}
+            fo : Graph  {suc c₁ } {c₁ ⊔ c₂}
             fo = forgetful.fobj {c₁} {c₂} (F a)
             vm : (y : vertex a ) →  vertex (g21 fo) 
-            vm y =  vmap (m21 fo) (ccc-from-graph.fobj a (atom y))
+            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 _)))
        pl : {c₁ c₂ : Level}  → (g : Graph {c₁} {c₂} ) → Category _ _ _
        pl g = PL g
        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 x ;
+             FObj = λ x →  {!!} ;
              FMap = λ {x} {y} h → {!!} ;
              isFunctor = {!!} } ;
              ccf = {!!} } where
-                  fvmap :  vertex g → vertex (g21 (forgetful.fobj c))
-                  fvmap = vmap f
-                  cobj : Obj Sets → Obj (cat c)
-                  cobj = {!!}