--- 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)