changeset 803:984d20c10c87

simpler graph to category
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Apr 2019 10:37:27 +0900
parents 7bc41fc7b563
children 2716d2945730
files CCChom.agda discrete.agda
diffstat 2 files changed, 91 insertions(+), 102 deletions(-) [+]
line wrap: on
line diff
--- a/CCChom.agda	Thu Apr 25 03:50:30 2019 +0900
+++ b/CCChom.agda	Thu Apr 25 10:37:27 2019 +0900
@@ -586,69 +586,75 @@
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl
 
-module ccc-from-graph ( Atom : Set ) ( homm : Atom → Atom → Set ) where
+module ccc-from-graph where
 
    open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
-
-   data objs : Set where
-      atom : Atom → objs
-      ⊤ : objs
-      _∧_ : objs → objs → objs
-      _<=_ : objs → objs → objs
-
-   data arrow  : objs → objs → Set where
-      hom : {a b : Atom} →  homm a b → arrow (atom a) (atom b)
-      id : (a : objs ) → arrow a a
-      ○ : (a : objs ) → arrow a ⊤
-      π : {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 } → arrow c a → arrow c b → arrow c (a ∧ b)
-      _・_ : {a b c : objs } → arrow b c → arrow a b → arrow a c
-      _* : {a b c : objs } → arrow (c ∧ b ) a → arrow c ( a <= b )
-
    open import discrete
    open graphtocat
 
+   open Graph
+
+   data Objs {G : Graph } : Set where
+      atom : (obj G) → Objs
+      ⊤ : Objs
+      _∧_ : Objs {G} → Objs {G} → Objs
+      _<=_ : Objs {G} → Objs {G} → Objs
+
+   data Arrow {G : Graph } :  Objs {G} → Objs {G} → Set where
+      arrow : {a b : obj G} →  (hom G) a b → Arrow (atom a) (atom b)
+      id : (a : Objs ) → Arrow a a
+      ○ : (a : Objs ) → Arrow a ⊤
+      π : {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 } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
+      _・_ : {a b c : Objs } → Arrow b c → Arrow a b → Arrow a c
+      _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
+
+
    -- positive intutionistic calculus
-   DX :   Category  Level.zero Level.zero Level.zero   
-   DX = GraphtoCat objs arrow
+   DX : (G : Graph) → Category  Level.zero Level.zero Level.zero   
+   DX G = GraphtoCat ( record { obj = Objs {G} ; hom = Arrow {G}} )
 
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-   CS : Functor DX (Sets {Level.zero})
-   FObj CS (atom x) = Atom
+   CS : {G : Graph } → Functor (DX G) (Sets {Level.zero})
+   FObj (CS {G}) (atom x) = obj G
    FObj CS ⊤ = One'
    FObj CS (x ∧ x₁) =  FObj CS x /\ FObj CS  x₁ 
    FObj CS (x <= x₁) = FObj CS x₁ → FObj CS x
    FMap CS {a} {.a} (id a) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero})
-   FMap CS {a} {b} (mono (x ・ y )) = Sets [ FMap CS (mono x) o FMap CS (mono y) ]
-   FMap CS {atom a} {atom b} (mono (hom f)) = λ x → b 
-   FMap CS {a} {.a} (mono (id a)) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero})
-   FMap CS {a} {⊤} (mono (○ a)) = λ x → OneObj'
-   FMap CS {(b ∧ _)} {b} (mono π) = proj₁
-   FMap CS {(_ ∧ b)} {b} (mono π') = proj₂
-   FMap CS {((b <= _) ∧ _)} {b} (mono ε) = λ x → ( proj₁ x ) ( proj₂ x )
-   FMap CS {a} {(_ ∧ _)} (mono < f , g >) = λ x → ( FMap CS (mono f) x , FMap CS (mono g) x )
-   FMap CS {a} {(_ <= _)} (mono (f *)) = λ x → λ y → FMap CS (mono f) ( x , y )
-   FMap CS {a} {⊤} (connected x f) = λ x → OneObj'
-   FMap CS {a} {b} (connected x f) = Sets [ FMap CS (mono x) o FMap CS f ]
+   FMap CS {a} {b} (next (x ・ y )) = Sets [ FMap CS (next x) o FMap CS (next y) ]
+   FMap CS {atom a} {atom b} (next (arrow f)) = λ x → b 
+   FMap CS {a} {.a} (next (id a)) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero})
+   FMap CS {a} {⊤} (next (○ a)) = λ x → OneObj'
+   FMap CS {(b ∧ _)} {b} (next π) = proj₁
+   FMap CS {(_ ∧ b)} {b} (next π') = proj₂
+   FMap CS {((b <= _) ∧ _)} {b} (next ε) = λ x → ( proj₁ x ) ( proj₂ x )
+   FMap CS {a} {(_ ∧ _)} (next < f , g >) = λ x → ( FMap CS (next f) x , FMap CS (next g) x )
+   FMap CS {a} {(_ <= _)} (next (f *)) = λ x → λ y → FMap CS (next f) ( x , y )
    isFunctor CS = isf where
        distrCS : {a b c : Obj DX } { g : Hom DX b c } { f : Hom DX a b } → Sets [ FMap CS (DX [ g o f ]) ≈ Sets [ FMap CS g o FMap CS f ] ]
        distrCS {a} {.a} {.a} {id a} {id a} = refl
-       distrCS {a} {b} {.b} {id b} {mono x} = refl
-       distrCS {a} {b} {.b} {id b} {connected x g} = refl
-       distrCS {a} {.(atom _)} {.(atom _)} {mono (hom x)} {g} = {!!}
-       distrCS {a} {.a₁} {.a₁} {mono (id a₁)} {g} = {!!}
-       distrCS {a} {.a₁} {.⊤} {mono (○ a₁)} {g} = {!!}
-       distrCS {a} {.(c ∧ _)} {c} {mono π} {g} = {!!}
-       distrCS {a} {.(_ ∧ c)} {c} {mono π'} {g} = {!!}
-       distrCS {a} {.((c <= _) ∧ _)} {c} {mono ε} {g} = {!!}
-       distrCS {a} {b} {.(_ ∧ _)} {mono < x , x₁ >} {g} = {!!}
-       distrCS {a} {b} {c} {mono (x ・ x₁)} {g} = {!!}
-       distrCS {a} {b} {.(_ <= _)} {mono (x *)} {g} = {!!}
-       distrCS {a} {b} {c} {connected x f} {g} = {!!}
+       distrCS {a} {b} {.b} {id b} {next x} = refl
+       distrCS {.(atom b)} {atom b} {atom c} {next (arrow x)} {id .(atom b)} = refl
+       distrCS {a} {atom b} {atom c} {next (arrow x)} {next x₁} = {!!}
+       distrCS {a} {atom(b)} {atom(c)} {next (arrow x)} {next x1} = extensionality Sets ( λ y → begin
+             FMap CS (DX [ next (arrow x) o next x1 ]) y
+          ≡⟨ {!!} ⟩
+             c
+          ≡⟨⟩
+             FMap CS (next (arrow x)) ( FMap CS (next x1) y)
+          ∎ ) where open ≡-Reasoning 
+       distrCS {a} {.a₁} {.a₁} {next (id a₁)} {g} = {!!}
+       distrCS {a} {.a₁} {.⊤} {next (○ a₁)} {g} = {!!}
+       distrCS {a} {.(c ∧ _)} {c} {next π} {g} = {!!}
+       distrCS {a} {.(_ ∧ c)} {c} {next π'} {g} = {!!}
+       distrCS {a} {.((c <= _) ∧ _)} {c} {next ε} {g} = {!!}
+       distrCS {a} {b} {.(_ ∧ _)} {next < x , x₁ >} {g} = {!!}
+       distrCS {a} {b} {c} {next (x ・ x₁)} {g} = {!!}
+       distrCS {a} {b} {.(_ <= _)} {next (x *)} {g} = {!!}
        isf : IsFunctor DX Sets (FObj CS) ( FMap CS ) 
        IsFunctor.identity isf = extensionality Sets ( λ x → refl )
        IsFunctor.distr isf = distrCS
--- a/discrete.agda	Thu Apr 25 03:50:30 2019 +0900
+++ b/discrete.agda	Thu Apr 25 10:37:27 2019 +0900
@@ -6,71 +6,54 @@
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
 
-
+record Graph : Set (Level.suc Level.zero ) where
+  field
+    obj : Set
+    hom : obj  → obj → Set
 
 module graphtocat where
 
-  data Arrow { obj : Set } { hom : obj → obj → Set } : ( a b : obj ) → Set where
-    id : ( a : obj ) → Arrow a a
-    mono : { a b : obj } → hom a b → Arrow a b
-    connected : {a b : obj } → {c : obj} → hom b c →  Arrow {obj} {hom} a b → Arrow a c
+  open import Relation.Binary.PropositionalEquality 
 
-  _+_ : { obj : Set } { hom : obj → obj → Set } {a b c : obj   } (f : (Arrow {obj} {hom} b c )) → (g : (Arrow {obj} {hom} a b )) → Arrow {obj} {hom} a c
-  id a + id .a = id a
-  id b + mono x = mono x
-  id a + connected x y = connected x y
-  mono x + id a = mono x
-  mono x + mono y = connected x (mono y)
-  mono x + connected y z = connected x ( connected y z )
-  connected x y + z = connected x ( y + z )
+  data Chain { g : Graph } : ( a b : Graph.obj g ) → Set where
+       id : ( a : Graph.obj g ) → Chain a a
+       next : { a b c : Graph.obj g } → (Graph.hom g b c ) → Chain {g} a b → Chain  a c
 
-  assoc-+ : { obj : Set } { hom : obj → obj → Set }  {a b c d : obj   }
-       (f : (Arrow  {obj} {hom} c d )) → (g : (Arrow {obj} {hom} b c )) → (h : (Arrow {obj} {hom} a b )) →
-       ( f + (g + h)) ≡  ((f + g) + h )
-  assoc-+ (id a) (id .a) (id .a) = refl
-  assoc-+ (id a) (id .a) (mono x) = refl
-  assoc-+ (id a) (id .a) (connected h h₁) = refl
-  assoc-+ (id a) (mono x) (id a₁) = refl
-  assoc-+ (id a) (mono x) (mono x₁) = refl
-  assoc-+ (id a) (mono x) (connected h h₁) = refl
-  assoc-+ (id a) (connected g h) _ = refl
-  assoc-+ (mono x) (id a) (id .a) = refl
-  assoc-+ (mono x) (id a) (mono x₁) = refl
-  assoc-+ (mono x) (id a) (connected h h₁) = refl
-  assoc-+ (mono x) (mono x₁) (id a) = refl
-  assoc-+ (mono x) (mono x₁) (mono x₂) = refl
-  assoc-+ (mono x) (mono x₁) (connected h h₁) = refl
-  assoc-+ (mono x) (connected g g₁) _ = refl
-  assoc-+ (connected f g) (x) (y) = cong (λ k → connected f k) (assoc-+ g x y )
-
-  open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
-
-  GraphtoCat : ( obj : Set ) ( hom : obj → obj → Set ) →  Category  Level.zero Level.zero Level.zero   
-  GraphtoCat  obj hom  = record {
-            Obj  = obj ;
-            Hom = λ a b →   Arrow a b  ;
-            _o_ =  λ{a} {b} {c} x y → _+_  x y ;
+  GraphtoCat : (G : Graph )  →  Category  Level.zero Level.zero Level.zero   
+  GraphtoCat G = record {
+            Obj  = Graph.obj G ;
+            Hom = λ a b →  Chain {G} 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
+                    identityL  = identityL; 
+                    identityR  = identityR ; 
+                    o-resp-≈  = o-resp-≈  ; 
+                    associative  = λ{a b c d f g h } → associative  f g h
                }
            }  where
-                identityL :   {A B : obj } {f : ( Arrow    A B) } →  ((id B)  + f)  ≡ f
-                identityL {_} {_} {id a} = refl
-                identityL {_} {_} {mono x} = refl
-                identityL {_} {_} {connected x f} = refl
-                identityR :   {A B : obj } {f : ( Arrow {obj} {hom}  A B) } →   ( f + id A )  ≡ f
-                identityR {_} {_} {id a} = refl
-                identityR {_} {_} {mono x} = refl
-                identityR {_} {_} {connected x f} =  cong (λ k → connected x k) ( identityR {_} {_} {f} )
-                o-resp-≈ :   {A B C : obj   } {f g :  ( Arrow    A B)} {h i : ( Arrow B C)} →
-                    f  ≡ g → h  ≡ i → ( h + f )  ≡ ( i + g )
-                o-resp-≈     {a} {b} {c} {f} {.f} {h} {.h}  refl refl = refl
+               open Chain
+               obj = Graph.obj G
+               hom = Graph.hom G
+               _++_ : {a b c : obj } (f : Chain {G} b c ) → (g : Chain {G} a b) → Chain {G} a c
+               id _ ++ f = f
+               (next x f) ++ g = next x ( f ++ g )
+
+               identityL : {A B : Graph.obj G} {f : Chain A B} → (id B ++ f) ≡ f
+               identityL = refl
+               identityR : {A B : Graph.obj G} {f : Chain A B} → (f ++ id A) ≡ f
+               identityR {a} {_} {id a} = refl
+               identityR {a} {b} {next x f} = cong ( λ k → next x k ) ( identityR {_} {_} {f} )
+               o-resp-≈  : {A B C : Graph.obj G} {f g : Chain A B} {h i : Chain B C} →
+                            f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
+               o-resp-≈  refl refl = refl
+               associative : {a b c d : Graph.obj G} (f : Chain c d) (g : Chain b c) (h : Chain a b) →
+                            (f ++ (g ++ h)) ≡ ((f ++ g) ++ h)
+               associative (id a) g h = refl
+               associative (next x f) g h = cong ( λ k → next x k ) ( associative f g h )
+
 
 
 data  TwoObject   : Set  where
@@ -95,7 +78,7 @@
    arrow-g :  TwoHom t0 t1
 
 TwoCat' : Category  Level.zero Level.zero Level.zero
-TwoCat'  = GraphtoCat TwoObject TwoHom 
+TwoCat'  = GraphtoCat ( record { obj = TwoObject ; hom = TwoHom } )
    where open graphtocat
 
 _×_ :  {a b c : TwoObject } →  TwoHom   b c  →  TwoHom   a b   →  TwoHom   a c 
@@ -167,7 +150,7 @@
 open import Data.Empty
 
 DiscreteCat' : (S : Set) → Category  Level.zero Level.zero Level.zero
-DiscreteCat'  S = GraphtoCat S ( λ _ _ →  ⊥  )
+DiscreteCat'  S = GraphtoCat ( record { obj = S ; hom = ( λ _ _ →  ⊥  ) } )
    where open graphtocat 
 
 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S)