--- a/limit-to.agda	Sat Mar 05 13:20:36 2016 +0900
+++ b/limit-to.agda	Sat Mar 05 14:52:49 2016 +0900
@@ -15,8 +15,8 @@
 ---          f
 ---       ------>
 ---     0         1
----       <------
----          frev
+---       ------>
+---          g
 ---          
 ---          
 ---          
@@ -51,35 +51,50 @@
          hom← : TwoObject  -> Hom Two ( obj← t0 ) ( obj← t1)
          hom-iso : {a :  Hom Two ( obj← t0 ) ( obj← t1)} -> hom← ( hom→ a) ≡ a
          hom-rev : {a : TwoObject } -> hom→ ( hom← a) ≡ a
+         hom-conv :  (x y : Obj Two) -> Hom Two x y -> Hom Two (obj← t0) (obj← t1)
 
 open TwoCat
 
-record TwoFunctor  {ℓ c₁ c₂ : Level  } (I A : Category  c₁ c₂ ℓ) (two : TwoCat I) ( Γ : Functor I A ) ( a b : Obj A ) 
-           ( f g : Hom A  a b )
-                          : Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
-    field
-          Γa :  FObj Γ (obj← two t0)   ≡ a 
-          Γb :  FObj Γ (obj← two t1)   ≡ b 
-          Γmap :  Hom A a b  -> Hom A (FObj Γ (obj← two t0)) (FObj Γ (obj← two t1))
-          Γmap-rev :  Hom A (FObj Γ (obj← two t0)) (FObj Γ (obj← two t1)) -> Hom A a b  
-          Γf :  A [ FMap Γ (hom← two t0)   ≈ Γmap f ]
-          Γg :  A [ FMap Γ (hom← two t1)   ≈ Γmap g ]
+indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (Two : Category c₁ c₂ ℓ) (two : TwoCat Two ) -> 
+        ( a b : Obj A ) ( f g : Hom A a b ) ( f-rev : Hom A b a ) 
+        -> Functor Two A
+indexFunctor A Two two a b f g f-rev = record {
+         FObj = λ a → fobj a
+       ; FMap = λ f → fmap f
+       ; isFunctor = record {
+             identity = {!!} 
+             ; distr = {!!}
+             ; ≈-cong = {!!}
+       }
+      } where
+          fobj : Obj Two -> Obj A
+          fobj x with  obj→ two x
+          ... | t0 = a
+          ... | t1 = b
+          fmap' :  (x y : Obj Two) -> TwoObject -> Hom A a b
+          fmap' _ _ t0 = f
+          fmap' _ _ t1 = g
+          fmap :  {x y : Obj Two } -> Hom Two x y -> Hom A (fobj x) (fobj y)
+          fmap {x} {y} f' with obj→ two x | obj→ two y 
+          ... | t0 | t0 = id1 A a
+          ... | t1 | t0 = f-rev
+          ... | t1 | t1 = id1 A b
+          ... | t0 | t1  = fmap' x y (hom→ two (hom-conv two x y f'))
 
-open TwoFunctor
 open Limit
 
 lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
       (Two : Category c₁ c₂ ℓ) (two : TwoCat Two ) 
       (lim : (I : Category c₁ c₂ ℓ) ( Γ : 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 )
-        → (  Γ : Functor Two A ) (  Γ-two : TwoFunctor Two A two  Γ a b f g)
+        →  {a b c : Obj A}  (f-rev : Hom A b 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 {c₁} A Two two lim {a} {b} {c}  f g Γ Γ-two e fe=ge = record {
+lim-to-equ {c₁} A Two two lim {a} {b} {c} f-rev 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
+         Γ = indexFunctor A Two two a b f g f-rev
          nmap :  (x : Obj Two) ( d : Obj A ) -> Hom A (FObj (K A Two d) x) (FObj Γ x)
          nmap x d with (obj→  two x)
          ... | t0 = ?