--- a/limit-to.agda	Sat Mar 05 07:20:03 2016 +0900
+++ b/limit-to.agda	Sat Mar 05 08:23:46 2016 +0900
@@ -1,22 +1,13 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 
-module limit-to {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-  where
+module limit-to where
 
 open import cat-utility
 open import HomReasoning
 open import Relation.Binary.Core
-open import Category.Sets
 open Functor
 
-open import Data.Nat hiding ( _⊔_ ) renaming ( suc to succ )
-open import Data.Bool
-
-open import Data.Fin as Fin
-  using (Fin; Fin′; #_; toℕ) renaming (_ℕ-ℕ_ to _-_ ; zero to Fzero ; suc to Fsuc )
-
-
 
 -- If we have limit then we have equalizer                                                                                                                                                                  
 ---  two objects category
@@ -28,48 +19,52 @@
 ---          g
 
 
-data TwoObject {c₁}  : Set c₁ where
+data TwoObject   : Set where
    t0 : TwoObject 
    t1 : TwoObject 
 
 
-record TwoCat  {ℓ c₁ c₂ : Level  } (Two : Category  c₁ c₂ ℓ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+record TwoCat  {ℓ c₁ c₂ : Level  } (Two : Category  c₁ c₂ ℓ) : Set  (c₂ ⊔ c₁ ⊔ ℓ)  where
     field
-         hom→ : Obj Two  -> TwoObject {ℓ}
-         hom← : TwoObject {ℓ} -> Obj Two
+         hom→ : Obj Two  -> TwoObject 
+         hom← : TwoObject  -> Obj Two
          hom-iso : {a : Obj Two} -> hom← ( hom→ a) ≡ a
-         hom-rev : {a : TwoObject {ℓ} } -> hom→ ( hom← a) ≡ a
+         hom-rev : {a : TwoObject } -> hom→ ( hom← a) ≡ a
 
 
+open TwoCat
 open Limit
 
-lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
+lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
       (two : TwoCat A ) 
-      (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 {c₁} A I two lim {a} {b} {c} f g e fe=ge = record {
+      (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} {frev : 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 lim {a} {b} {c} {frev} 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 :  {!!}  → Obj A
+         Γobj :  TwoObject → Obj A
          Γobj t0 = a
          Γobj t1 = b
-         Γmap :  {!!}  → Hom A a b
-         Γmap t0 = f
-         Γmap t1 = g
-         Γ : Functor I A
+         Γmap :  (x : Obj A ) → (y : Obj A ) → Hom A x y →  Hom A (Γobj (hom→ two x)) (Γobj (hom→ two y))
+         Γmap  x y _ with  (hom→ two x) | (hom→ two y)  
+         ... | t0 | t0 = id1 A a
+         ... | t0 | t1 = f
+         ... | t1 | t0 = frev
+         ... | t1 | t1 = id1 A b
+         Γ : Functor A A
          Γ = record {
-            FObj  = λ x → Γobj {!!} ;
-            FMap  = λ f → {!!} ;
+            FObj  = λ x → ( Γobj ( hom→ two x ) ) ;
+            FMap  = λ {x} {y} f  → Γmap x y f ;
             isFunctor = record {
                      ≈-cong  = {!!} ; 
                     identity = {!!} ;
                     distr = {!!}
             }
           }
-         nat : (d : Obj A) → NTrans I A (K A I d) Γ
+         nat : (d : Obj A) → NTrans A A (K A A d) Γ
          nat d = record {
             TMap = λ x → {!!} ;
             isNTrans = record {
@@ -77,5 +72,5 @@
             }
           }
          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 (lim Γ {c} {nat c}) d (nat d) 
+         k {d} h fh=gh  = limit (lim A  Γ  {c} {nat c}) d (nat d)