Mercurial > hg > Members > kono > Proof > category

changeset 933:e702aa8be9dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
level try and CCC bad approach
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 14 May 2020 10:48:52 +0900
parents f19425b54aba
children cce9e539486e
files CCCGraph.agda
diffstat 1 files changed, 49 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Tue May 12 22:26:09 2020 +0900
+++ b/CCCGraph.agda	Thu May 14 10:48:52 2020 +0900
@@ -95,6 +95,8 @@
                 *-cong refl = refl
 
 
+
+
 open import graph
 module ccc-from-graph {c₁ c₂ : Level }  (G : Graph {c₁} {c₂})  where
 
@@ -127,6 +129,7 @@
    < f , g > ・ h = < f ・ h , g ・ h >
    iv f g ・ h = iv f ( g ・ h )
 
+
    identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
    identityL = refl
 
@@ -219,6 +222,31 @@
         IsFunctor.≈-cong isf refl = refl 
         IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
+   pccc : CCC PL  -- this does not work because of ≡ , if we define another equality, o-resp-≈ may trouble
+   pccc = record {
+         １  = ⊤
+       ; ○ = λ _ → ○ _
+       ; _∧_ = _∧_ 
+       ; <_,_> = λ f g → < f , g >
+       ; π = iv π (id  _)
+       ; π' = iv π' (id _)
+       ; _<=_ = _<=_
+       ; _* = λ f → iv (f *) (id _)
+       ; ε = iv ε (id _)
+       ; isCCC = isCCC
+     } where
+         open graphtocat.Chain 
+         isCCC : CCC.IsCCC PL ⊤ ○ _∧_ <_,_> (iv π (id  _)) (iv π' (id _)) _<=_ (λ f → iv (f *) (id _)) (iv ε (id _))
+         isCCC = record {
+               e2  = {!!} --e2
+             ; e3a = {!!} --λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g}
+             ; e3b = {!!} --λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g}
+             ; e3c = {!!} --e3c
+             ; π-cong = {!!} --π-cong
+             ; e4a = {!!} --e4a
+             ; e4b = {!!} --e4b
+             ; *-cong = {!!} --*-cong
+           } 
 
 ---
 ---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap 
@@ -342,15 +370,15 @@
              g'
           ∎  )
   
-  fobj : Obj Cart → Obj Grph
+  fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ}) → Obj Grph
   fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
-  fmap :  {a b : Obj (Cart   ) } → Hom (Cart ) a b → Hom (Grph  ) ( fobj a ) ( fobj b )
+  fmap :  {c₁ c₂ ℓ : Level}  {a b : Obj (Cart {c₁} {c₂} {ℓ}  ) } → Hom (Cart ) a b → Hom (Grph  ) ( fobj a ) ( fobj b )
   fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }
 
-  UX :  Functor Cart Grph
-  FObj UX a = fobj a
-  FMap UX f =  fmap f
-  isFunctor UX  = isf where
+  UX :  {c₁ c₂ : Level} → Functor (Cart  {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) (Grph {c₁} {c₂})
+  FObj UX a = {!!} -- fobj a
+  FMap UX f =  {!!} -- fmap f
+  isFunctor UX  = {!!} where -- isf where
     isf : IsFunctor Cart Grph fobj fmap
     IsFunctor.identity isf {a} {b} {f} e = mrefl refl
     IsFunctor.distr isf {a} {b} {c} f = mrefl refl
@@ -371,10 +399,10 @@
 Sets0 : {c₂ : Level } → Category (suc c₂) c₂ c₂
 Sets0 {c₂} = Sets {c₂}
 
-ccc-graph-univ :  UniversalMapping Grph Cart forgetful.UX 
-ccc-graph-univ = record {
-     F = λ g → csc {!!}   ;
-     η = λ a → record { vmap = λ y →  graphtocat.Chain {!!} {!!} {!!}  ; emap = λ f x →  {!!} } ; -- 
+ccc-graph-univ :  {c₁ c₂ : Level} → UniversalMapping (Grph {c₁} {c₂}) (Cart {suc (c₁ ⊔ c₂)} {c₁ ⊔ c₂} {c₁ ⊔ c₂}) forgetful.UX 
+ccc-graph-univ {c₁} {c₂} = record {
+     F = F ;
+     η = η ; -- λ a → record { vmap = λ y →  graphtocat.Chain {!!} {!!} {!!}  ; emap = λ f x →  {!!} } ; -- 
      _* = solution ;
      isUniversalMapping = record {
          universalMapping = {!!} ;
@@ -383,14 +411,20 @@
   } where
        open forgetful  
        open ccc-from-graph
-       csc : {c₁ c₂ : Level}  → Graph {c₂} {c₁}  → Obj Cart  
-       csc {c₁} {c₂}  g = record { cat = Sets {c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } 
+       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 x → {!!} }
+       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
        pl : {c₁ c₂ : Level}  → (g : Graph {c₁} {c₂} ) → Category _ _ _
        pl g = PL g
-       cobj  :  {g : Obj Grph } {c : Obj Cart} → Hom Grph g (FObj UX c)  → Objs g → Obj (cat c)
-       cobj {g} {c} f (atom x) = vmap f x
+       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 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) 
@@ -403,7 +437,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 {!!} {!!}
+       solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (csc g) c
        solution  {g} {c} f = {!!} -- record { cmap = record { FObj = λ x → {!!} ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }