--- a/discrete.agda	Wed Sep 26 10:00:02 2018 +0900
+++ b/discrete.agda	Wed Sep 26 20:17:09 2018 +0900
@@ -92,37 +92,31 @@
 
 -- Category with no arrow but identity
 
-record DiscreteObj  {c₁  : Level } (S : Set c₁) :  Set c₁  where
-   field
-      obj : S              -- this is necessary to avoid single object
-
-open DiscreteObj
-
-record DiscreteHom { c₁ : Level} { S : Set c₁} (a : DiscreteObj {c₁} S) (b : DiscreteObj {c₁} S) 
+record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S) 
       : Set c₁ where
    field
       discrete : a ≡ b     -- if f : a → b then a ≡ b
-   dom : DiscreteObj S
+   dom : S
    dom = a
 
 open DiscreteHom
 
-_*_ :  ∀ {c₁}  →  {S : Set c₁} {a b c : DiscreteObj {c₁} S} →  DiscreteHom {c₁}  b c  →  DiscreteHom {c₁}  a b   →  DiscreteHom {c₁}  a c 
+_*_ :  ∀ {c₁}  →  {S : Set c₁} {a b c : S} →  DiscreteHom {c₁}  b c  →  DiscreteHom {c₁}  a b   →  DiscreteHom {c₁}  a c 
 _*_ {_}  {a} {b} {c}  x y = record {discrete = trans ( discrete y) (discrete x) }
 
-DiscreteId : { c₁ : Level} { S : Set c₁} ( a : DiscreteObj {c₁} S ) →  DiscreteHom {c₁}  a a
+DiscreteId : { c₁ : Level} { S : Set c₁} ( a : S ) →  DiscreteHom {c₁}  a a
 DiscreteId a = record { discrete = refl }
 
 open  import  Relation.Binary.PropositionalEquality
 
-assoc-* :   {c₁  : Level } { S : Set c₁} {a b c d : DiscreteObj  {c₁}  S}
+assoc-* :   {c₁  : Level } { S : Set c₁} {a b c d : S}
        {f : (DiscreteHom  c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} →
        dom ( f * (g * h)) ≡ dom ((f * g) * h )
 assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl
 
 DiscreteCat : {c₁ : Level  } →  (S : Set c₁) → Category   c₁   c₁   c₁  
 DiscreteCat   {c₁}  S = record {
-    Obj  = DiscreteObj  {c₁} S ;
+    Obj  = S ;
     Hom = λ a b →   DiscreteHom  {c₁} {S} a b  ;
     _o_ =  λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ;
     _≈_ =  λ x y → dom x  ≡ dom y ;   -- x ≡ y does not work because refl ≡ discrete f is failed as it should be
@@ -135,11 +129,11 @@
             associative  = λ{a b c d f g h } → assoc-*  { c₁} {S}  {a} {b} {c} {d} {f} {g} {h}
        }
    }  where
-        identityL :   {a b : DiscreteObj {c₁} S} {f : ( DiscreteHom {c₁}  a b) } →  dom ((DiscreteId b)  * f)  ≡ dom f
+        identityL :   {a b : S} {f : ( DiscreteHom {c₁}  a b) } →  dom ((DiscreteId b)  * f)  ≡ dom f
         identityL   {a} {b} {f} = refl
-        identityR :   {A B : DiscreteObj S} {f : ( DiscreteHom {c₁}   A B) } →  dom ( f * DiscreteId A )  ≡ dom f
+        identityR :   {A B : S} {f : ( DiscreteHom {c₁}   A B) } →  dom ( f * DiscreteId A )  ≡ dom f
         identityR   {a} {b} {f} = refl
-        o-resp-≈ :   {A B C : DiscreteObj  S } {f g :  ( DiscreteHom {c₁}   A B)} {h i : ( DiscreteHom B C)} →
+        o-resp-≈ :   {A B C : S } {f g :  ( DiscreteHom {c₁}   A B)} {h i : ( DiscreteHom B C)} →
             dom f  ≡ dom g → dom h  ≡ dom i → dom ( h * f )  ≡ dom ( i * g )
         o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  refl refl = refl