--- a/limit-to.agda	Wed Apr 01 17:37:04 2015 +0900
+++ b/limit-to.agda	Thu Apr 02 22:49:13 2015 +0900
@@ -20,41 +20,43 @@
 ---       ------>
 ---          g
 
-data  _∨_  {c₁} (A B : Set c₁): Set c₁ where
-        or1 :  A → A ∨ B
-        or2 :  B → A ∨ B
-
-
-record TwoSet {c₁} (A : Set c₁): Set (suc c₁) where
-    field
-            a0 : A
-            a1 : A
-            element : (x : A) → ( x ≡ a0) ∨ (x ≡ a1 )
-            
-
-data Two {c₁}  : Set c₁ where
-   t0 : Two 
-   t1 : Two 
-
 
 infixr 40 _::_
 data  List {a} (A : Set a)  : Set a where
    [] : List A
    _::_ : A -> List A -> List A
 
--- record TwoCat {ℓ} (S : Sets {ℓ}) : Set ℓ where
---    field
---         twoSet : TwoSet S
---         hom : TwoSet S → TwoSet S → Set _
+
+postulate id-0 id-1 f g : Set  c₂
 
 
-twocat : {c₁ c₂ ℓ : Level} → (id-0 id-1 f g : Set  c₂) → Category c₁ _ ℓ
-twocat {c₁} {c₂} {ℓ} id-0 id-1 f g = record {
+data Two {c₁}  : Set c₁ where
+   t0 : Two 
+   t1 : Two 
+
+record Two-Hom {c₁} (a : Two  {c₁}) (b : Two  {c₁}) : Set (c₁ ⊔ suc c₂ ⊔ ℓ) where
+   field
+       Map    : Set  c₂
+
+hom : Two {c₁} → Two {c₁} → List (Set  c₂)
+hom t0 t0 =  id-0 :: []
+hom t0 t1 =  f :: g :: []
+hom t1 t0 =  []
+hom t1 t1 =  id-1 :: []
+
+Two-id :  {c₁ : Level} -> (a : Two {c₁}) ->  Two-Hom {c₁} a a
+Two-id {c₁} t0  = record { Map = id-0 }
+Two-id {c₁} t1  = record { Map = id-1 }
+
+open Two-Hom
+
+twocat : {c₁ ℓ : Level} → Category c₁ _ ℓ
+twocat {c₁} {ℓ} = record {
     Obj  = Two {c₁} ;
-    Hom = λ a b →  List (Set  c₂) ;
+    Hom = λ a b →  Two-Hom a b   ; 
     _o_ =  {!!} ;
     _≈_ = {!!} ;
-    Id  = {!!} ;
+    Id  =  \{a} -> Two-id a ;
     isCategory  = record {
             isEquivalence = {!!} ;
             identityL  = {!!} ;
@@ -63,11 +65,6 @@
             associative  = {!!}
        } 
    } where
-        hom : Two {c₁} → Two {c₁} → List (Set  c₂)
-        hom t0 t0 =  id-0 :: []
-        hom t0 t1 =  f :: g :: []
-        hom t1 t0 =  []
-        hom t1 t1 =  id-1 :: []
 
 open Limit