--- a/limit-to.agda	Fri Mar 03 12:12:06 2017 +0900
+++ b/limit-to.agda	Sat Mar 04 10:43:17 2017 +0900
@@ -38,7 +38,7 @@
 
 -- Functor Γ : TwoCat -> A
 
-IndexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat {c₁} {c₂})  A
+IndexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat  {c₁} {c₂}) A
 IndexFunctor  {c₁} {c₂} {ℓ} A a b f g = record {
          FObj = λ a → fobj a
        ; FMap = λ {a} {b} f → fmap {a} {b} f
@@ -48,7 +48,7 @@
              ; ≈-cong = λ {a} {b} {c} {f}   → ≈-cong  {a} {b} {c} {f}
        }
       } where
-          T = TwoCat {c₁} {c₂}
+          T = TwoCat   {c₁} {c₂}
           fobj :  Obj T → Obj A
           fobj t0 = a
           fobj t1 = b
@@ -109,14 +109,14 @@
 IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
         →  {a b : Obj A}      (f g : Hom A  a b )
     (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → 
-        NTrans (TwoCat {c₁} {c₂}) A (K A (TwoCat {c₁} {c₂}) d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
+        NTrans TwoCat  A (K A TwoCat  d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
 IndexNat {c₁} {c₂} {ℓ} A {a} {b} f g d h fh=gh = record {
     TMap = λ x → nmap x d h ;
     isNTrans = record {
         commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh 
     }
  } where
-         I = TwoCat {c₁} {c₂}
+         I = TwoCat  {c₁} {c₂}
          Γ : Functor I A
          Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
          nmap :  (x : Obj I ) ( d : Obj (A)  ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x)
@@ -152,12 +152,12 @@
                 ∎
 
 
-equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂  ℓ) {a b : Obj A} -> (f g : Hom A a b)  (comp : Complete A (TwoCat {c₁} {c₂} )) -> 
-         Hom A ( limit-c comp (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)) a
-equlimit {c₁} {c₂} {ℓ} A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)) t0
+equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂  ℓ) {a b : Obj A} -> (f g : Hom A a b)  (comp : Complete A TwoCat ) -> 
+         Hom A ( limit-c comp (IndexFunctor A a b f g)) a
+equlimit A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor A a b f g)) t0
 
 lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-      (comp : Complete A (TwoCat {c₁} {c₂} ) )
+      (comp : Complete A TwoCat  )
         →  {a b : Obj A}  (f g : Hom A  a b ) 
         → (fe=ge : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ] ) 
         → IsEqualizer A (equlimit A f g comp) f g
@@ -167,22 +167,28 @@
         ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
      } where
-         I = TwoCat {c₁} {c₂}
+         I : Category  c₁ c₂ c₂ 
+         I = TwoCat 
          Γ : Functor I A
-         Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
+         Γ = IndexFunctor A a b f g
+         e : Hom A (limit-c comp (IndexFunctor A a b f g)) a
          e = equlimit A f g comp
+         c : Obj A 
          c = limit-c comp Γ
+         natL : NTrans I A (K A I c) Γ
          natL = limit-u comp Γ
-         eqlim =  isLimit comp  Γ 
+         lim : Limit A I Γ c natL
+         lim =  isLimit comp  Γ 
+         nat0 : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ
          nat0 = IndexNat A f g 
          k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
-         k {d} h fh=gh  =  limit eqlim d (nat0 d h fh=gh )
+         k {d} h fh=gh  =  limit lim d (nat0 d h fh=gh )
          ek=h :  (d : Obj A ) (h : Hom A d a ) →  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  → A [ A [ e o k h fh=gh ] ≈ h ]
          ek=h d h fh=gh = let open  ≈-Reasoning A in  begin
                     e o k h fh=gh
                 ≈⟨⟩
                     TMap (limit-u comp Γ) t0  o k h fh=gh
-                ≈⟨ t0f=t eqlim {d} {nat0 d h fh=gh } {t0}  ⟩
+                ≈⟨ t0f=t lim {d} {nat0 d h fh=gh } {t0}  ⟩
                     TMap (nat0 d h fh=gh) t0
                 ≈⟨⟩
                     h
@@ -221,7 +227,7 @@
                 → A [ A [ e o k' ] ≈ h ] → A [ k h  fh=gh   ≈ k' ]
          uniquness d h fh=gh k' ek'=h =  let open  ≈-Reasoning A in  begin
                     k h fh=gh
-                ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
+                ≈⟨ limit-uniqueness lim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
                     k'
                 ∎