--- a/limit-to.agda	Wed Dec 24 12:00:16 2014 +0900
+++ b/limit-to.agda	Wed Dec 24 12:50:52 2014 +0900
@@ -20,30 +20,53 @@
 ---       ------>
 ---          g
 
-record TwoCat  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-      (a b : Obj A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+data Two {c₁}  : Set c₁ where
+   t0 : Two 
+   t1 : Two 
+
+record TwoCat  {c₁ c₂ ℓ : Level} (I : Category c₁ c₂ ℓ) 
+      (two : Two {c₁}) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
    field
-       f→ : Obj A → Hom A a b
-       f← : Hom A a b → Obj A
-       unique-f :  (f←  (f→  a) )  ≡ a
-       g→ : Obj A → Hom A a b
-       g← : Hom A a b → Obj A
-       unique-g :  (g←  (g→  b) )  ≡ b
+       obj  : Two {c₁}  → Obj I
+       obj← : Obj I → Two  
+       map  : Two {c₁} → Hom I (obj t0) (obj t1) 
+       map← : Hom I (obj t0) (obj t1) → Two {c₁}  
+       unique-obj  :  ∀{two : Two } → obj← ( obj two ) ≡ two
+       unique-obj1 :  ∀{i : Obj I } → obj ( obj← i ) ≡ i
+       unique-map  :  ∀{two : Two } → map← ( map two ) ≡ two
+       unique-map1 :  ∀{f : Hom I (obj t0) (obj t1) } → map ( map← f ) ≡ f
 
 
 open Limit
+open TwoCat
 
 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
-      ( i0 i1 : Obj I) 
-      (two : TwoCat I i0 i1) ( Γ : Functor I A )
+      (two : Two  ) 
+      (twocat : TwoCat I two) 
       (lim : ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness
         →  {a b c : Obj A} (f g : Hom A a b)  → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
-lim-to-equ A I i0 i1 two Γ lim {a} {b} {c} f g e fe=ge = record {
+lim-to-equ {c₁} A I two twocat lim {a} {b} {c} f g e fe=ge = record {
         fe=ge =  fe=ge
         ; k = λ {d} h fh=gh → k {d} h fh=gh
         ; ek=h = λ {d} {h} {fh=gh} → {!!}
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!}
      } where
+         Γobj :  Two {c₁} → Obj A
+         Γobj t0 = a
+         Γobj t1 = b
+         Γmap :  Two {c₁} → Hom A a b
+         Γmap t0 = f
+         Γmap t1 = g
+         Γ : Functor I A
+         Γ = record {
+            FObj  = λ x → Γobj (obj← twocat x) ;
+            FMap  = λ f → {!!} ;
+            isFunctor = record {
+                     ≈-cong  = {!!} ; 
+                    identity = {!!} ;
+                    distr = {!!}
+            }
+          }
          nat : (d : Obj A) → NTrans I A (K A I d) Γ
          nat d = record {
             TMap = λ x → {!!} ;