Mercurial > hg > Members > kono > Proof > category

changeset 945:94ece478b583

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cobj and cmap connected
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 17 May 2020 23:07:18 +0900
parents c58684b15d97
children f8e6e9128f3d
files CCCGraph.agda
diffstat 1 files changed, 46 insertions(+), 32 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sun May 17 18:42:17 2020 +0900
+++ b/CCCGraph.agda	Sun May 17 23:07:18 2020 +0900
@@ -369,50 +369,50 @@
           → {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₂}) → Obj Grph
-  fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
-  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 )) } 
+  uobj : Obj (Cart {suc c₁ } {c₁ ⊔ c₂} {c₁ ⊔ c₂}) → Obj Grph
+  uobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
+  umap :  {a b : Obj (Cart {suc c₁ } {c₁ ⊔ c₂} {c₁ ⊔ c₂} ) } → Hom (Cart ) a b → Hom (Grph {c₁} {c₂}) (g21 ( uobj a )) (g21 ( uobj b ))
+  umap {a} {b} f =  record {
+           vmap = λ e → vmap (m21 (uobj b)) (FObj (cmap f) (vmap (m12 (uobj a)) e ))
+         ; emap = λ e → emap (m21 (uobj b)) (FMap (cmap f) (emap (m12 (uobj a)) e )) } 
 
   UX :  Functor (Cart  {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {c₁} {c₂})
-  FObj UX a = g21 (fobj a)
-  FMap UX f =  fmap f
+  FObj UX a = g21 (uobj a)
+  FMap UX f =  umap f
   isFunctor UX  = isf where
-    isf : IsFunctor Cart Grph (λ z → g21 (fobj z)) fmap
+    isf : IsFunctor Cart Grph (λ z → g21 (uobj z)) umap
     IsFunctor.identity isf {a} {b} {f} = begin
-         fmap (id1 Cart a) 
+         umap (id1 Cart a) 
        ≈⟨⟩
-         fmap {a} {a} (record { cmap = identityFunctor ; ccf = λ x → x })
+         umap {a} {a} (record { cmap = identityFunctor ; ccf = λ x → x })
        ≈⟨⟩
-         record { vmap = λ e → vmap (m21 (fobj a)) (vmap (m12 (fobj a)) e ) ; emap = λ e → emap (m21 (fobj a)) (emap (m12 (fobj a)) e )}
-       ≈⟨ giso← {fobj a} {f} {f}  ⟩
+         record { vmap = λ e → vmap (m21 (uobj a)) (vmap (m12 (uobj a)) e ) ; emap = λ e → emap (m21 (uobj a)) (emap (m12 (uobj a)) e )}
+       ≈⟨ giso← {uobj a} {f} {f}  ⟩
          record { vmap = λ y → y ; emap = λ f → f }
        ≈⟨⟩
-         id1 Grph (g21 (fobj a))
+         id1 Grph (g21 (uobj a))
        ∎ where open ≈-Reasoning Grph 
     IsFunctor.distr isf {a} {b} {c} {f} {g} = begin
-         fmap ( Cart [ g o f ] )
+         umap ( Cart [ g o f ] )
        ≈⟨⟩
-         ( m21 (fobj c) & ( record { vmap = λ e → FObj (cmap (( Cart [ g o f ] ))) e ; emap = λ e → FMap (cmap (( Cart [ g o f ] ))) e} &  m12 (fobj a) ) )
+         ( m21 (uobj c) & ( record { vmap = λ e → FObj (cmap (( Cart [ g o f ] ))) e ; emap = λ e → FMap (cmap (( Cart [ g o f ] ))) e} &  m12 (uobj a) ) )
        ≈⟨ {!!} ⟩
---         ( m21 (fobj c) &  (record { vmap = λ e → FObj (cmap g) (FObj (cmap f) e)  ; emap = λ e → FMap (cmap g) (FMap (cmap f) e) }
---            &  m12 (fobj a)))
---       ≈⟨ cdr (cdr (car (giso← {fobj b} )))  ⟩
---         ( m21 (fobj c) &  (record { vmap = λ e → FObj (cmap g) e ; emap = λ e → FMap (cmap g) e}
---            &  ((m12 (fobj b) 
---            &  (m21 (fobj b))) &  (record { vmap = λ e → FObj (cmap f) e ; emap = λ e → FMap (cmap f) e}
---            &  (m12 (fobj a) )))))
+--         ( m21 (uobj c) &  (record { vmap = λ e → FObj (cmap g) (FObj (cmap f) e)  ; emap = λ e → FMap (cmap g) (FMap (cmap f) e) }
+--            &  m12 (uobj a)))
+--       ≈⟨ cdr (cdr (car (giso← {uobj b} )))  ⟩
+--         ( m21 (uobj c) &  (record { vmap = λ e → FObj (cmap g) e ; emap = λ e → FMap (cmap g) e}
+--            &  ((m12 (uobj b) 
+--            &  (m21 (uobj b))) &  (record { vmap = λ e → FObj (cmap f) e ; emap = λ e → FMap (cmap f) e}
+--            &  (m12 (uobj a) )))))
 --       ≈⟨⟩
-         Grph [ fmap g o fmap f ]
+         Grph [ umap g o umap f ]
        ∎ where open ≈-Reasoning Grph 
     IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = {!!} where -- lemma ( (extensionality Sets ( λ z → lemma4 (
           --       ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
           --  )))) (f=g e) where
-      lemma4 : {x y : vertex (fobj b)} →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
+      lemma4 : {x y : vertex (uobj b)} →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
       lemma4 (refl eqv) = refl 
-      -- lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ g21 (fobj b)] emap (fmap f) {!!} == emap (fmap g) {!!}
+      -- lemma : vmap (umap f) ≡ vmap (umap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ g21 (uobj b)] emap (umap f) {!!} == emap (umap g) {!!}
       -- lemma = {!!} -- refl (refl eqv) = mrefl (≡←≈ b eqv)
 
 
@@ -431,7 +431,7 @@
   FCat : Obj (Cart {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
   FCat  = record { cat = record {
           Obj = Obj PL 
-          ; Hom = λ a b → fobj a → fobj b
+          ; Hom = λ a b → Hom B (FObj CS a) (FObj CS b)
           ; _o_ = Category._o_ B
           ; _≈_ = Category._≈_ B
           ; Id  = λ {a} → id1 B (FObj CS a)
@@ -478,16 +478,30 @@
        η : (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₂}
-            fo = forgetful.fobj {c₁} {c₂} (F a)
+            fo = uobj {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) (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 _)))
+            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
+       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 (m12 (uobj {c₁} {c₂} c)) (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} {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} {⊤} 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 {!!})
        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 = λ {x} {y} h → {!!} ;
+             FObj = λ x →  cobj {g} {c} f x ;
+             FMap = λ {x} {y} h → c-map {g} {c} {x} {y} f h ;
              isFunctor = {!!} } ;
              ccf = {!!} } where