Mercurial > hg > Members > kono > Proof > category

changeset 935:92f8f57467e3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add fig
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 15 May 2020 17:59:15 +0900
parents cce9e539486e
children d13e0981e667
files CCCGraph.agda
diffstat 1 files changed, 36 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Thu May 14 18:28:08 2020 +0900
+++ b/CCCGraph.agda	Fri May 15 17:59:15 2020 +0900
@@ -368,8 +368,24 @@
   FMap UX f =  fmap f
   isFunctor UX  = isf where
     isf : IsFunctor Cart Grph (λ z → g21 (fobj z)) fmap
-    IsFunctor.identity isf {a} {b} {f} e = {!!}
-    IsFunctor.distr isf {a} {b} {c} f = {!!}
+    eff : (a : Obj Cart) (f : vertex (g21 (fobj a)) ) → edge (g21 (fobj a)) f f
+    eff a f = {!!}
+    IsFunctor.identity isf {a} {b} {f} = begin
+         fmap (id1 Cart a) 
+       ≈⟨⟩
+         fmap {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} {eff a f } ⟩
+         record { vmap = λ y → y ; emap = λ f → f }
+       ≈⟨⟩
+         id1 Grph (g21 (fobj a))
+       ∎ where open ≈-Reasoning Grph 
+    IsFunctor.distr isf {a} {b} {c} {f} {g} = begin
+         fmap ( Cart [ g o f ] )
+       ≈⟨ {!!} ⟩
+         Grph [ fmap g o fmap 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
@@ -399,16 +415,26 @@
   } where
        open forgetful  
        open ccc-from-graph
+       --                                        η : Hom Grph a (FObj UX (F a))
+       --                    f : edge g x y   ----------------------------------->  g21 (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
+       --                          |                                                       | 
+       --                          | Functor (CS g)                                        | 
+       --                          ↓                                                       |
+       --  Sets  ((z : vertx g) → C z x)  ----> ((z : vertx g) → C z y)  = h : Hom Sets (fobj (atom x)) (fobj (atom y))
+       --
+       cs : {c₁ c₂ : Level}  → (g : Graph  {c₁} {c₂} ) → Functor  (ccc-from-graph.PL g) (Sets {_})
+       cs g = CS g
        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 } 
-       FO : (a : Obj (Grph {c₁} {c₂}) ) → Graph {(c₁ ⊔ c₂)} {(c₁ ⊔ c₂)}
-       FO a = FObj UX (F a)
        η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a))
-       η a =  record { vmap = λ y →  {!!} ;  emap = λ f → {!!} }
-       csc : Graph  → Obj Cart  
-       csc g = record { cat = Sets {c₁ ⊔ c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } 
-       cs : {c₁ c₂ : Level}  → (g : Graph  {c₁} {c₂} ) → Functor  (ccc-from-graph.PL g) (Sets {_})
-       cs g = CS g
+       η a = record { vmap = λ y → {!!} y ;  emap = λ f → {!!} } where
+       --    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)
@@ -425,7 +451,7 @@
        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 (csc g) c
+       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 = {!!} }