--- a/discrete.agda	Tue Apr 23 06:39:24 2019 +0900
+++ b/discrete.agda	Tue Apr 23 11:30:34 2019 +0900
@@ -7,7 +7,73 @@
 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
 
 
-data  TwoObject {c₁ : Level}  : Set c₁ where
+
+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
+
+  _+_ : { 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 )
+
+  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 ;
+            _≈_ =  λ 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
+                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
+
+
+data  TwoObject   : Set  where
    t0 : TwoObject
    t1 : TwoObject
 
@@ -22,20 +88,24 @@
 --
 --     missing arrows are constrainted by TwoHom data
 
-data TwoHom {c₁ c₂ : Level } : TwoObject {c₁}  → TwoObject {c₁} → Set c₂ where
+data TwoHom  : TwoObject   → TwoObject  → Set  where
    id-t0 :    TwoHom t0 t0
    id-t1 :    TwoHom t1 t1
    arrow-f :  TwoHom t0 t1
    arrow-g :  TwoHom t0 t1
 
+TwoCat' : Category  Level.zero Level.zero Level.zero
+TwoCat'  = GraphtoCat TwoObject TwoHom 
+   where open graphtocat
 
-_×_ :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  TwoHom {c₁} {c₂} b c  →  TwoHom {c₁} {c₂} a b   →  TwoHom {c₁} {c₂} a c 
-_×_ {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-f  = arrow-f 
-_×_ {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-g  = arrow-g 
-_×_ {_}  {_}  {t1} {t1} {t1}  id-t1   id-t1    = id-t1 
-_×_ {_}  {_}  {t0} {t0} {t1}  arrow-f id-t0    = arrow-f 
-_×_ {_}  {_}  {t0} {t0} {t1}  arrow-g id-t0    = arrow-g 
-_×_ {_}  {_}  {t0} {t0} {t0}  id-t0   id-t0    = id-t0 
+_×_ :  {a b c : TwoObject } →  TwoHom   b c  →  TwoHom   a b   →  TwoHom   a c 
+_×_ {t0} {t1} {t1}  id-t1   arrow-f  = arrow-f 
+_×_ {t0} {t1} {t1}  id-t1   arrow-g  = arrow-g 
+_×_ {t1} {t1} {t1}  id-t1   id-t1    = id-t1 
+_×_ {t0} {t0} {t1}  arrow-f id-t0    = arrow-f 
+_×_ {t0} {t0} {t1}  arrow-g id-t0    = arrow-g 
+_×_ {t0} {t0} {t0}  id-t0   id-t0    = id-t0 
+
 
 open TwoHom
 
@@ -44,56 +114,62 @@
 --
 --   It can be proved without TwoHom constraints
 
-assoc-× :   {c₁  c₂ : Level } {a b c d : TwoObject  {c₁} }
-       {f : (TwoHom {c₁}  {c₂ } c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} →
+assoc-× :    {a b c d : TwoObject   }
+       {f : (TwoHom    c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} →
        ( f × (g × h)) ≡ ((f × g) × h )
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0   }{ id-t0   }{ id-t0   } = refl
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0   }{ id-t0   } = refl
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0   }{ id-t0   } = refl
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1   }{ arrow-f }{ id-t0   } = refl
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1   }{ arrow-g }{ id-t0   } = refl
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-f } = refl
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-g } = refl
-assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ id-t1   } = refl
+assoc-×   {t0} {t0} {t0} {t0} { id-t0   }{ id-t0   }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t0} {t1} { arrow-f }{ id-t0   }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t0} {t1} { arrow-g }{ id-t0   }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t1} {t1} { id-t1   }{ arrow-f }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t1} {t1} { id-t1   }{ arrow-g }{ id-t0   } = refl
+assoc-×   {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-f } = refl
+assoc-×   {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-g } = refl
+assoc-×   {t1} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ id-t1   } = refl
 
-TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) →  (TwoHom {c₁}  {c₂ } a a )
-TwoId {_} {_} t0 = id-t0 
-TwoId {_} {_} t1 = id-t1 
+TwoId :   (a : TwoObject   ) →  (TwoHom    a a )
+TwoId  t0 = id-t0 
+TwoId   t1 = id-t1 
 
 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
 
-TwoCat : {c₁ c₂ : Level  } →  Category   c₁  c₂  c₂
-TwoCat   {c₁}  {c₂} = record {
+TwoCat :  Category  Level.zero Level.zero Level.zero   
+TwoCat      = record {
     Obj  = TwoObject ;
     Hom = λ a b →   TwoHom a b  ;
-    _o_ =  λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
     _≈_ =  λ x y → x  ≡ y ;
     Id  =  λ{a} → TwoId a ;
     isCategory  = record {
             isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
-            identityL  = λ{a b f} → identityL {c₁}  {c₂ } {a} {b} {f} ;
-            identityR  = λ{a b f} → identityR {c₁}  {c₂ } {a} {b} {f} ;
-            o-resp-≈  = λ{a b c f g h i} →  o-resp-≈  {c₁}  {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
-            associative  = λ{a b c d f g h } → assoc-×   {c₁}  {c₂} {a} {b} {c} {d} {f} {g} {h}
+            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-×      {a} {b} {c} {d} {f} {g} {h}
        }
    }  where
-        identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  ((TwoId B)  × f)  ≡ f
-        identityL  {c₁}  {c₂}  {t1} {t1} { id-t1 } = refl
-        identityL  {c₁}  {c₂}  {t0} {t0} { id-t0 } = refl
-        identityL  {c₁}  {c₂}  {t0} {t1} { arrow-f } = refl
-        identityL  {c₁}  {c₂}  {t0} {t1} { arrow-g } = refl
-        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   ( f × TwoId A )  ≡ f
-        identityR  {c₁}  {c₂}  {t1} {t1} { id-t1  } = refl
-        identityR  {c₁}  {c₂}  {t0} {t0} { id-t0 } = refl
-        identityR  {c₁}  {c₂}  {t0} {t1} { arrow-f } = refl
-        identityR  {c₁}  {c₂}  {t0} {t1} { arrow-g } = refl
-        o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  ( TwoHom {c₁}  {c₂ } A B)} {h i : ( TwoHom B C)} →
+        identityL :   {A B : TwoObject } {f : ( TwoHom    A B) } →  ((TwoId B)  × f)  ≡ f
+        identityL      {t1} {t1} { id-t1 } = refl
+        identityL      {t0} {t0} { id-t0 } = refl
+        identityL      {t0} {t1} { arrow-f } = refl
+        identityL      {t0} {t1} { arrow-g } = refl
+        identityR :   {A B : TwoObject } {f : ( TwoHom    A B) } →   ( f × TwoId A )  ≡ f
+        identityR      {t1} {t1} { id-t1  } = refl
+        identityR      {t0} {t0} { id-t0 } = refl
+        identityR      {t0} {t1} { arrow-f } = refl
+        identityR      {t0} {t1} { arrow-g } = refl
+        o-resp-≈ :   {A B C : TwoObject   } {f g :  ( TwoHom    A B)} {h i : ( TwoHom B C)} →
             f  ≡ g → h  ≡ i → ( h × f )  ≡ ( i × g )
-        o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {.f} {h} {.h}  refl refl = refl
+        o-resp-≈     {a} {b} {c} {f} {.f} {h} {.h}  refl refl = refl
 
 
 -- Category with no arrow but identity
 
+
+open import Data.Empty
+
+DiscreteCat' : (S : Set) → Category  Level.zero Level.zero Level.zero
+DiscreteCat'  S = GraphtoCat S ( λ _ _ →  ⊥  )
+   where open graphtocat 
+
 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S) 
       : Set c₁ where
    field