Mercurial > hg > Members > kono > Proof > category

changeset 911:b8c5f15ee561

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
small graph and small category on CCC to graph
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 02 May 2020 03:40:56 +0900
parents 8f41ad966eaa
children 635418b4b2f3
files CCCGraph.agda
diffstat 1 files changed, 146 insertions(+), 146 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Fri May 03 17:11:33 2019 +0900
+++ b/CCCGraph.agda	Sat May 02 03:40:56 2020 +0900
@@ -94,132 +94,129 @@
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl
 
-module ccc-from-graph where
+open import graph
+module ccc-from-graph {c₁  c₂  : Level} (G : Graph {c₁} {c₂} )  where
 
    open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
-   open import graph
-   open graphtocat 
-
    open Graph
 
-   data Objs (G : Graph {Level.zero} {Level.zero} ) : Set where    -- formula
-      atom : (vertex G) → Objs G
-      ⊤ : Objs G
-      _∧_ : Objs G → Objs G → Objs G
-      _<=_ : Objs G → Objs G → Objs G
+   data Objs : Set c₁ where
+      atom : (vertex G) → Objs 
+      ⊤ : Objs 
+      _∧_ : Objs  → Objs  → Objs 
+      _<=_ : Objs → Objs → Objs 
 
-   data Arrow (G : Graph ) :  Objs G → Objs G → Set where  --- proof
-      arrow : {a b : vertex G} →  (edge G) a b → Arrow G (atom a) (atom b)
-      ○ : (a : Objs G ) → Arrow G a ⊤
-      π : {a b : Objs G } → Arrow G ( a ∧ b ) a
-      π' : {a b : Objs G } → Arrow G ( a ∧ b ) b
-      ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a
-      <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b)
-      _* : {a b c : Objs G } → Arrow G (c ∧ b ) a → Arrow G c ( a <= b )
+   data  Arrows  : (b c : Objs ) → Set ( c₁  ⊔  c₂ ) 
+   data Arrow :  Objs → Objs → Set (c₁ ⊔ c₂)  where                       --- case i
+      arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
+      π : {a b : Objs } → Arrow ( a ∧ b ) a
+      π' : {a b : Objs } → Arrow ( a ∧ b ) b
+      ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
+      _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b )        --- case v
+
+   data  Arrows where
+      id : ( a : Objs ) → Arrows a a                                      --- case i
+      ○ : ( a : Objs ) → Arrows a ⊤                                       --- case i
+      <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b)      -- case iii
+      iv  : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c   -- cas iv
 
-   data one {v : Level} {S : Set v} : Set v where
-             elm : (x : S ) → one 
+   _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
+   id a ・ g = g
+   ○ a ・ g = ○ _
+   < f , g > ・ h = < f ・ h , g ・ h >
+   iv f g ・ h = iv f ( g ・ h )
 
-   iso→ : {v : Level} {S : Set v} → one → S
-   iso→ (elm x) = x
+   identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
+   identityL = refl
 
-   data iso← {v : Level} {S : Set v} : (one {v} {S} ) → S → Set v where
-       elmeq : {x : S} →  iso←  ( elm x ) x
+   identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
+   identityR {a} {a} {id a} = refl
+   identityR {a} {⊤} {○ a} = refl 
+   identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR identityR
+   identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR
 
-   iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso← x a → iso→ x ≡ a
-   iso-left (elm x) .x elmeq = refl
-
-   iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x ) 
-   iso-right (elm x) = elmeq
+   assoc≡ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
+                            (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
+   assoc≡ (id a) g h = refl
+   assoc≡ (○ a) g h = refl 
+   assoc≡ < f , f₁ > g h =  cong₂ (λ j k → < j , k > ) (assoc≡ f g h) (assoc≡ f₁ g h) 
+   assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h )
 
---   record one {v : Level} {S : Set v} : Set (suc v) where
---      field
---         elm : S
+   -- positive intutionistic calculus
+   PL :  Category  c₁  (c₁ ⊔ c₂) (c₁ ⊔ c₂)
+   PL = record {
+            Obj  = Objs;
+            Hom = λ a b →  Arrows  a b ;
+            _o_ =  λ{a} {b} {c} x y → x ・ y ;
+            _≈_ =  λ x y → x ≡  y ;
+            Id  =  λ{a} → id a ;
+            isCategory  = record {
+                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym} ;
+                    identityL  = λ {a b f} → identityL {a} {b} {f} ; 
+                    identityR  = λ {a b f} → identityR {a} {b} {f} ; 
+                    o-resp-≈  = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}  ; 
+                    associative  = λ{a b c d f g h } → assoc≡  f g h
+               }
+           } where  
+              o-resp-≈  : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
+                                    f ≡  g → h ≡  i → (h ・ f) ≡ (i ・ g)
+              o-resp-≈ refl refl = refl
+
+--------
 --
---   iso→ : {v : Level} {S : Set v} → one {v} {S} → One {Level.zero} → S
---   iso→ x OneObj = one.elm x
---   iso← : {v : Level} {S : Set v} → one {v} {S} → S → One {Level.zero}
---   iso← x y = OneObj
+-- Functor from Positive Logic to Sets
 --
---   iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso→ x ( iso← x a ) ≡ a
---   iso-left x a =  {!!}
---
---   iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x OneObj ) ≡ OneObj
---   iso-right x =  refl
+
+   -- open import Category.Sets
+   -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂
+
+   C = graphtocat.Chain G
 
-   record one' {v : Level} {S : Set v} : Set (suc v) where
-     field
-        elm' : S
-        iso→' : One {Level.zero} → S
-        iso←' : S → One {Level.zero}
-        iso-left' : iso→' ( iso←' elm' ) ≡ elm'
-        iso-right' : iso←' ( iso→' OneObj ) ≡ OneObj
+   tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
+   tr f x y  = graphtocat.next f (x y) 
+   
+   fobj :  ( a  : Objs  ) → Set (c₁ ⊔ c₂ )
+   fobj  (atom x) = ( y : vertex G ) → C y x
+   fobj ⊤ = One
+   fobj  (a ∧ b) = ( fobj  a /\ fobj  b)
+   fobj  (a <= b) = fobj  b → fobj  a
+
+   fmap :  { a b : Objs  } → Hom PL a b → fobj  a → fobj  b
+   amap :  { a b : Objs  } → Arrow  a b → fobj  a → fobj  b
+   amap  (arrow x) =  tr x
+   amap π ( x , y ) = x 
+   amap π' ( x , y ) = y
+   amap ε (f , x ) = f x
+   amap (f *) x = λ y →  fmap f ( x , y ) 
+   fmap (id a) x = x
+   fmap (○ a) x = OneObj
+   fmap < f , g > x = ( fmap f x , fmap g x )
+   fmap (iv x f) a = amap x ( fmap f a )
 
-   tmp : {v : Level} {S : Set v} → one {v} {S}  → one' {v} {S}
-   tmp x = record {
-         elm' = iso→ x
-       ; iso→' = λ _ → iso→ x
-       ; iso←' = λ _ → OneObj
-       ; iso-left' = refl
-       ; iso-right' = refl
-     }
-     
+--   CS is a map from Positive logic to Sets
+--    Sets is CCC, so we have a cartesian closed category generated by a graph
+--       as a sub category of Sets
+
+   CS :  Functor PL (Sets {c₁ ⊔ c₂ })
+   FObj CS a  = fobj  a
+   FMap CS {a} {b} f = fmap  {a} {b} f
+   isFunctor CS = isf where
+        _+_ = Category._o_ PL
+        ++idR = IsCategory.identityR ( Category.isCategory PL )
+        distr : {a b c : Obj PL}  { f : Hom PL a b } { g : Hom PL b c } → (z : fobj  a ) → fmap (g + f) z ≡ fmap g (fmap f z)
+        distr {a} {a₁} {a₁} {f} {id a₁} z = refl
+        distr {a} {a₁} {⊤} {f} {○ a₁} z = refl
+        distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k  →  j , k  ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z)
+        distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr  {a} {b} {d} {f} {g} z) x where 
+           adistr : fmap (g + f) z ≡ fmap g (fmap f z) →
+                ( x : Arrow d c ) → fmap ( iv x (g + f) ) z  ≡ fmap ( iv x g ) (fmap f z )
+           adistr eq x = cong ( λ k → amap x k ) eq
+        isf : IsFunctor PL Sets fobj fmap 
+        IsFunctor.identity isf = extensionality Sets ( λ x → refl )
+        IsFunctor.≈-cong isf refl = refl 
+        IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
 
-   record SM {v : Level} : Set (suc v)  where
-      field
-        graph : Graph  {v} {v}
-        sobj : vertex graph → Set
-        smap : { a b : vertex graph } → edge graph a b  → sobj a → sobj b
-
-   open SM
-
-   -- positive intutionistic calculus
-   PL : (G : SM) → Graph
-   PL G = record { vertex = Objs (graph G) ; edge = Arrow (graph G) }
-   DX : (G : SM) → Category  Level.zero Level.zero Level.zero   
-   DX G = GraphtoCat (PL G)
-
-   -- open import Category.Sets
-   -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
-
-   fobj : {G : SM} ( a  : Objs (graph G) ) → Set
-   fobj {G} (atom x) = sobj G x
-   fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b )
-   fobj {G} (a <= b) = fobj {G} b → fobj {G} a
-   fobj ⊤ = One
-   amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
-   amap {G} (arrow x) = smap G x
-   amap (○ a) _ = OneObj
-   amap π ( x , _) = x
-   amap π'( _ , x) = x
-   amap ε ( f , x ) = f x
-   amap < f , g > x = (amap f x , amap g x)
-   amap (f *) x = λ y → amap f ( x , y )
-   fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
-   fmap {G} {a} (id a) = λ z → z
-   fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ]
-
-   --   CS is a map from Positive logic to Sets
-   --    Sets is CCC, so we have a cartesian closed category generated by a graph
-   --       as a sub category of Sets
-
-   CS : (G : SM ) → Functor (DX G) (Sets {Level.zero})
-   FObj (CS G) a  = fobj a
-   FMap (CS G) {a} {b} f = fmap {G} {a} {b} f
-   isFunctor (CS G) = isf where
-       _++_ = Category._o_ (DX G)
-       ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
-       distr : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
-       distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = adistr (distr {a} {b} {d} {f} {g} z ) x where
-          adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
-              ( x : Arrow (graph G) d c ) → fmap ( next x (g ++ f) ) z  ≡ fmap ( next x g ) (fmap f z )
-          adistr eq x = cong ( λ k → amap x k ) eq
-       distr {a} {b} {b} {f} {id b} z =  refl
-       isf : IsFunctor (DX G) Sets fobj fmap 
-       IsFunctor.identity isf = extensionality Sets ( λ x → refl )
-       IsFunctor.≈-cong isf refl = refl
-       IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
 ---
 ---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap 
@@ -233,6 +230,7 @@
 record CCCObj { c₁ c₂ ℓ  : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
    field
      cat : Category c₁ c₂ ℓ
+     ≡←≈ : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g
      ccc : CCC cat
  
 open CCCObj 
@@ -268,7 +266,7 @@
 open import graph
 open Graph
 
-record GMap {v v' : Level} (x y : Graph {v} {v'} )  : Set (suc (v ⊔ v') ) where
+record GMap {v v' : Level} (x y : Graph {v} {v'} )  : Set (v ⊔ v' ) where
   field
    vmap : vertex x → vertex y
    emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
@@ -288,8 +286,8 @@
 _&_ :  {v v' : Level} {x y z : Graph {v} {v'}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
 f & g = record { vmap = λ x →  vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) }
 
-Grp : {v v' : Level} → Category (suc (v ⊔ v')) (suc v ⊔ v') (suc ( v ⊔ v'))
-Grp {v} {v'} = record {
+Grph : {v v' : Level} → Category (suc (v ⊔ v')) (v ⊔ v') (suc ( v ⊔ v'))
+Grph {v} {v'} = record {
     Obj = Graph {v} {v'}
   ; Hom = GMap {v} {v'}
   ; _o_ = _&_
@@ -340,41 +338,43 @@
              g'
           ∎  )
   
-fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grp {c₁} {c₂})
+fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grph {c₁} {c₂})
 fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) }
-fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grp {c₁} {c₂}) ( fobj a ) ( fobj b )
+fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grph {c₁} {c₂}) ( fobj a ) ( fobj b )
 fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) }
 
-UX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) →  {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g  )
-    → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂})
-FObj (UX {c₁} {c₂} {ℓ} ≈-to-≡  ) a = fobj a
-FMap (UX ≈-to-≡)  f =  fmap f
-isFunctor (UX {c₁} {c₂} {ℓ}  ≈-to-≡)  = isf where
-  -- if we don't need ≈-cong ( i.e.   f ≈ g → UX f =m= UX g ), all lemmas are not necessary
-  open import HomReasoning
-  isf : IsFunctor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁} {c₂}) fobj fmap
-  IsFunctor.identity isf {a} {b} {f} e = mrefl refl 
-  IsFunctor.distr isf f = mrefl refl
-  IsFunctor.≈-cong isf {a} {b} {f} {g} eq {x} {y} e = lemma (extensionality Sets ( λ z → lemma4 (
-               ≃-cong (cat b) (eq (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
-          ))) (eq e) where
-      lemma4 : {x y : vertex (fobj 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 → [ fobj b ] emap (fmap f) e == emap (fmap g) e
-      lemma refl (refl eqv) = mrefl ( ≈-to-≡ (cat b) eqv )
+UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂}  )
+FObj UX a = fobj a
+FMap UX f =  fmap f
+isFunctor UX  = 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
+  IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = 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 (refl eqv) = refl 
+    lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e
+    lemma refl (refl eqv) = mrefl (≡←≈ b eqv)
 
 
----   
----   open ccc-from-graph
----   
----   sm : {v : Level } → Graph {v} → SM {v}
----   SM.graph (sm g) = g
----   SM.sobj (sm  g) = {!!}
----   SM.smap (sm  g) = {!!}
----   
----   HX : {v : Level } ( x : Obj (Grp {v}) ) → Obj (Grp {v})
----   HX {v} x = {!!} -- FObj UX ( record { cat = Sets {v} ;  ccc = sets } )
----   
----   
----   
----   
+open ccc-from-graph.Objs
+open ccc-from-graph.Arrow
+open ccc-from-graph.Arrows
+open graphtocat.Chain
+
+ccc-graph-univ :  {c₁ : Level } → UniversalMapping (Grph {c₁} {c₁}  ) (Cart {c₁} {c₁} {c₁} ) UX
+ccc-graph-univ {c₁}   = record {
+     F = λ g → csc g ;
+     η = λ a → record { vmap = λ y → atom y ; emap = λ f x y →  next f (x y) } ;
+     _* = {!!} ;
+     isUniversalMapping = record {
+         universalMapping = {!!} ;
+         uniquness = {!!}
+      }
+  } where
+       csc : Graph → Obj Cart
+       csc g = record { cat = {!!} ; ccc = {!!} } where 
+           open ccc-from-graph g
+