# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556265258 -32400
# Node ID dd0d0a2019903605e8896565452c5bd67f6f1c98
# Parent  979c0bf97a5a64b0b355dafc21bbabdcec388bec
...

diff -r 979c0bf97a5a -r dd0d0a201990 CCChom.agda
--- a/CCChom.agda	Thu Apr 25 17:56:30 2019 +0900
+++ b/CCChom.agda	Fri Apr 26 16:54:18 2019 +0900
@@ -590,7 +590,7 @@
 
    open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
    open import discrete
-   open graphtocat
+   open graphtocat hiding ( _++_ )
 
    open Graph
 
@@ -611,33 +611,40 @@
       _・_ : {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 )
 
+   record SM  : Set (suc Level.zero)  where
+      field
+        graph : Graph 
+        sobj : vertex graph → Set
+        smap : { a b : vertex graph } → edge graph a b  → sobj a → sobj b
+
+   open SM
 
    -- positive intutionistic calculus
-   DX : (G : Graph) → Category  Level.zero Level.zero Level.zero   
-   DX G = GraphtoCat ( record { vertex = Objs {G} ; edge = Arrow {G}} )
+   DX : (G : SM) → Category  Level.zero Level.zero Level.zero   
+   DX G = GraphtoCat ( record { vertex = Objs {graph G} ; edge = Arrow {graph G}} )
 
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-   fobj : {G : Graph} ( a  : Obj (DX G) ) → Set
-   fobj {G} (atom x) = vertex G
-   fobj (a ∧ b) = (fobj a ) /\ (fobj b )
-   fobj (a <= b) = fobj b → fobj a
+   fobj : {G : SM} ( a  : Obj (DX 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'
    {-# TERMINATING #-}
-   fmap : {G : Graph} { a b : Obj (DX G) } → Hom (DX G) a b → fobj a → fobj b
-   fmap {G} {a} {a} (id a) = id1 Sets (fobj a) where open ≈-Reasoning (Sets {Level.zero})
-   fmap {G} {a} {(atom b)} (next (arrow x) f) = λ _ → b
+   fmap : {G : SM} { a b : Obj (DX G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
+   fmap {G} {a} {a} (id a) = λ z → z
+   fmap {G} {a} {(atom b)} (next (arrow x) f) = λ z → smap G x ( fmap f z )
    fmap {G} {a} {b} (next (id b) f) = fmap f
    fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
-   fmap {G} {a} {b} (next π f) = λ z → proj₁ ( fmap f z )
+   fmap {G} {a} {b} (next {a} {.b ∧ y} {b} π f) = λ z → proj₁ ( fmap f z )
    fmap {G} {a} {b} (next π' f) =  λ z → proj₂ ( fmap f z )
    fmap {G} {a} {b} (next ε f) =  λ z → (  proj₁ (fmap f z) )(  proj₂ (fmap f z) )
-   fmap {G} {a} {b} (next (f ・ g) h) = λ z →  fmap ( next f (next g h ) ) z
+   fmap {G} {a} {b} (next (f ・ g) h) =  λ z →  fmap (next f (next g h)) z
    fmap {G} {a} {(_ ∧ _)} (next < f , g > h) = λ z → ( fmap (next f h) z ,  fmap (next g h) z)
    fmap {G} {a} {(c <= b)} (next {_} {d} (f *) g ) = λ x y → fmap (next f (id (d ∧ b))) ( fmap g x , y )
 
-   CS : {G : Graph } → Functor (DX G) (Sets {Level.zero})
+   CS : {G : SM } → Functor (DX G) (Sets {Level.zero})
    FObj CS a  = fobj a
    FMap (CS {G}) {a} {b} f = fmap {G} {a} {b} f
    isFunctor (CS {G}) = isf where
@@ -654,27 +661,19 @@
              Sets [ fmap (next x g) o fmap (Chain.id a) ]
           ∎  where open ≈-Reasoning Sets
        distrCS {a} {b} {b} {f} {id b} = refl
-       distrCS {a} {b} {.(atom _)} {f} {next (arrow x) g} = refl
-       distrCS {a} {b} {c} {f} {next (id c) g} = begin
-             fmap (DX G [ next (Arrow.id c) g o f ])
-          ≈⟨ {!!} ⟩
-             Sets [ fmap (next (Arrow.id c) g) o fmap f ]
-          ∎  where open ≈-Reasoning Sets
+       distrCS {a} {b} {atom z} {f} {next (arrow x) g} = distrCS 
+       distrCS {a} {b} {c} {f} {next (id c) g} = distrCS 
        distrCS {a} {b} {.⊤} {f} {next (○ a₁) g} = begin
              fmap (DX G [ next (○ a₁) g o f ])
           ≈⟨ extensionality Sets ( λ x → refl ) ⟩
              Sets [ fmap (next (○ a₁) g) o fmap f ]
           ∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {c} {f} {next π g} = {!!}
-       distrCS {a} {b} {c} {f} {next π' g} = {!!}
-       distrCS {a} {b} {c} {f} {next ε g} = {!!}
-       distrCS {a} {b} {.(_ ∧ _)} {f} {next < x , x₁ > g} = {!!}
-       distrCS {a} {b} {c} {f} {next (x ・ x₁) g} = extensionality Sets ( λ z → begin
-             fmap (DX G [ next (x ・ x₁) g o f ]) z
-          ≡⟨ {!!} ⟩
-             ( Sets [ fmap (next (x ・ x₁) g) o fmap f ]  ) z
-          ∎ ) where open ≡-Reasoning 
-       distrCS {a} {b} {.(_ <= _)} {f} {next (x *) g} = {!!}
+       distrCS {a} {b} {c} {f} {next {.b} {c ∧ x} {c} π g} = distrCS
+       distrCS {a} {b} {c} {f} {next π' g} = distrCS
+       distrCS {a} {b} {c} {f} {next ε g} = distrCS
+       distrCS {a} {b} {.(_ ∧ _)} {f} {next < x , x₁ > g} = distrCS
+       distrCS {a} {b} {c} {f} {next (x ・ y) g} = distrCS
+       distrCS {a} {b} {.(_ <= _)} {f} {next (x *) g} = distrCS
        isf : IsFunctor (DX G) Sets fobj fmap 
        IsFunctor.identity isf = extensionality Sets ( λ x → refl )
        IsFunctor.≈-cong isf refl = refl
diff -r 979c0bf97a5a -r dd0d0a201990 discrete.agda
--- a/discrete.agda	Thu Apr 25 17:56:30 2019 +0900
+++ b/discrete.agda	Fri Apr 26 16:54:18 2019 +0900
@@ -19,6 +19,10 @@
        id : ( a : Graph.vertex g ) → Chain a a
        next : { a b c : Graph.vertex g } → (Graph.edge g b c ) → Chain {g} a b → Chain  a c
 
+  _++_ : { G : Graph} {a b c : Graph.vertex G } (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 )
+
   GraphtoCat : (G : Graph )  →  Category  Level.zero Level.zero Level.zero   
   GraphtoCat G = record {
             Obj  = Graph.vertex G ;
@@ -37,9 +41,6 @@
                open Chain
                obj = Graph.vertex G
                hom = Graph.edge 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.vertex G} {f : Chain A B} → (id B ++ f) ≡ f
                identityL = refl