# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556162523 -32400
# Node ID 2716d2945730f045063209c6c36e0e580d2464e9
# Parent  984d20c10c879cb96bc75dabc1319069c29d60d9
fix

diff -r 984d20c10c87 -r 2716d2945730 CCChom.agda
--- a/CCChom.agda	Thu Apr 25 10:37:27 2019 +0900
+++ b/CCChom.agda	Thu Apr 25 12:22:03 2019 +0900
@@ -595,13 +595,13 @@
    open Graph
 
    data Objs {G : Graph } : Set where
-      atom : (obj G) → Objs
+      atom : (vertex 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)
+      arrow : {a b : vertex G} →  (edge 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
@@ -614,49 +614,31 @@
 
    -- positive intutionistic calculus
    DX : (G : Graph) → Category  Level.zero Level.zero Level.zero   
-   DX G = GraphtoCat ( record { obj = Objs {G} ; hom = Arrow {G}} )
+   DX G = GraphtoCat ( record { vertex = Objs {G} ; edge = Arrow {G}} )
 
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
    CS : {G : Graph } → Functor (DX G) (Sets {Level.zero})
-   FObj (CS {G}) (atom x) = obj G
+   FObj (CS {G}) (atom x) = vertex 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} (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} {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 )
+   FObj CS (a ∧ b) = (FObj CS a ) /\ (FObj CS b )
+   FObj CS (a <= b) = FObj CS b → FObj CS a
+   FMap CS {a} {a} (id a) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero})
+   FMap CS {a} {(atom b)} (next (arrow x) f) = λ _ → b
+   FMap CS {a} {.a₁} (next (id a₁) f) = FMap CS f
+   FMap CS {a} {.⊤} (next (○ a₁) f) = λ _ → OneObj'
+   FMap CS {a} {b} (next π f) = λ z → proj₁ ( FMap CS f z )
+   FMap CS {a} {b} (next π' f) =  λ z → proj₂ ( FMap CS f z )
+   FMap CS {a} {b} (next ε f) =  λ z → (  proj₁ (FMap CS f z) )(  proj₂ (FMap CS f z) )
+   FMap CS {a} {.(_ ∧ _)} (next < f , g > h) = λ z → ( FMap CS (next f h) z ,  FMap CS (next g h) z)
+   FMap CS {a} {b} (next (f ・ g) h) = λ z →  FMap CS ( next f (next g h ) ) z
+   FMap CS {a} {(c <= b)} (next (e *) f) = {!!}
+   isFunctor (CS {G}) = isf where
+       distrCS : {a b c : Obj (DX G)} { g : Hom (DX G) b c } { f : Hom (DX G) a b } → Sets [ FMap CS ((DX G) [ g o f ]) ≈ Sets [ FMap CS g o FMap CS f ] ]
+       distrCS = {!!}
+       isf : IsFunctor (DX G) Sets (FObj CS) ( FMap CS ) 
+       IsFunctor.identity isf = extensionality Sets ( λ x → {!!} )
        IsFunctor.distr isf = distrCS
        IsFunctor.≈-cong isf refl = refl
 
diff -r 984d20c10c87 -r 2716d2945730 discrete.agda
--- a/discrete.agda	Thu Apr 25 10:37:27 2019 +0900
+++ b/discrete.agda	Thu Apr 25 12:22:03 2019 +0900
@@ -8,20 +8,20 @@
 
 record Graph : Set (Level.suc Level.zero ) where
   field
-    obj : Set
-    hom : obj  → obj → Set
+    vertex : Set
+    edge : vertex  → vertex → Set
 
 module graphtocat where
 
   open import Relation.Binary.PropositionalEquality 
 
-  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
+  data Chain { g : Graph } : ( a b : Graph.vertex g ) → Set where
+       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
 
   GraphtoCat : (G : Graph )  →  Category  Level.zero Level.zero Level.zero   
   GraphtoCat G = record {
-            Obj  = Graph.obj G ;
+            Obj  = Graph.vertex G ;
             Hom = λ a b →  Chain {G} a b ;
             _o_ =  λ{a} {b} {c} x y → x ++ y ;
             _≈_ =  λ x y → x  ≡ y ;
@@ -35,21 +35,21 @@
                }
            }  where
                open Chain
-               obj = Graph.obj G
-               hom = Graph.hom G
+               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.obj G} {f : Chain A B} → (id B ++ f) ≡ f
+               identityL : {A B : Graph.vertex 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 B : Graph.vertex 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} →
+               o-resp-≈  : {A B C : Graph.vertex 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) →
+               associative : {a b c d : Graph.vertex 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 )
@@ -78,7 +78,7 @@
    arrow-g :  TwoHom t0 t1
 
 TwoCat' : Category  Level.zero Level.zero Level.zero
-TwoCat'  = GraphtoCat ( record { obj = TwoObject ; hom = TwoHom } )
+TwoCat'  = GraphtoCat ( record { vertex = TwoObject ; edge = TwoHom } )
    where open graphtocat
 
 _×_ :  {a b c : TwoObject } →  TwoHom   b c  →  TwoHom   a b   →  TwoHom   a c 
@@ -150,7 +150,7 @@
 open import Data.Empty
 
 DiscreteCat' : (S : Set) → Category  Level.zero Level.zero Level.zero
-DiscreteCat'  S = GraphtoCat ( record { obj = S ; hom = ( λ _ _ →  ⊥  ) } )
+DiscreteCat'  S = GraphtoCat ( record { vertex = S ; edge = ( λ _ _ →  ⊥  ) } )
    where open graphtocat 
 
 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S)