--- a/limit-to.agda	Thu Mar 17 11:26:22 2016 +0900
+++ b/limit-to.agda	Sun Mar 20 11:36:44 2016 +0900
@@ -1,7 +1,7 @@
 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
@@ -33,47 +33,49 @@
    arrow-g :  Arrow
    nil :  Arrow
 
-record RawHom {c₁ ℓ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set  (c₁  ⊔ ℓ) where
+record RawHom { c₁ c₂ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set   c₂ where
    field
-       RawMap    : Arrow  {ℓ }
+       RawMap    : Arrow  { c₂ }
 
 open RawHom
 
-record Two-Hom { c₁  ℓ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set   (c₁  ⊔ ℓ)  where
+record Two-Hom { c₁  c₂ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set    c₂  where
    field
-      hom : Maybe ( RawHom { c₁}  {ℓ } a b )
+      hom : Maybe ( RawHom  {c₁} { c₂ } a b )
 
 open  Two-Hom 
 
-Two-id :  {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { ℓ} a a 
+Two-id :  { c₁ c₂ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { c₂}  a a 
 Two-id _  = record { hom = just ( record { RawMap = id-t0 } ) }
 
 -- arrow composition
 
-twocomp : {c₁ ℓ : Level } ->  { a b : TwoObject {c₁} } -> Arrow  {ℓ } -> Arrow  {ℓ } -> Maybe  ( RawHom a b )
+twocomp : {c₁  c₂ : Level } ->  { a b : TwoObject {c₁} } -> Arrow  { c₂ } -> Arrow  { c₂ } -> Maybe  ( RawHom a b )
 twocomp id-t0 f = just ( record { RawMap = f } )
 twocomp f id-t0 = just ( record { RawMap = f } )
 twocomp _ _ = nothing
 
-_×_ :  { c₁  ℓ : Level }  -> {A B C : TwoObject { c₁} } →  Two-Hom { c₁}  {ℓ}  B C →  Two-Hom { c₁}  {ℓ}  A B  →  Two-Hom { c₁}  {ℓ}  A C 
+_×_ :  { c₁  c₂ : Level }  -> {A B C : TwoObject { c₁} } →  Two-Hom { c₁}  {c₂}  B C →  Two-Hom { c₁}  {c₂}  A B  →  Two-Hom { c₁}  {c₂}  A C 
 _×_   { c₁} {ℓ} {a} {b} {c} f g with  hom f |  hom g 
 _×_   { c₁} {ℓ} {a} {b} {c} f g | nothing   | _ = record { hom = nothing }
 _×_   { c₁} {ℓ} {a} {b} {c} f g | _   | nothing  = record { hom = nothing }
 _×_   { c₁} {ℓ} {a} {b} {c} _ _ | just f  | just g   = record { hom = twocomp  { c₁} {ℓ} {a} {c} (RawMap f) (RawMap g ) }
 
-_==_ :  {c₁ ℓ : Level } ->  {a b : TwoObject  {c₁} } -> Rel (Maybe (RawHom  {c₁} {ℓ} a b  )) (ℓ ⊔ c₁)
+_==_ :  {c₁ c₂ : Level } ->  {a b : TwoObject  {c₁} } -> Rel (Maybe (RawHom  {c₁} {c₂} a b  )) c₂
 _==_    =   Eq ( _≡_  ) 
 
+open import maybeCat  
+
 
-TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  (ℓ ⊔ c₁)  (ℓ ⊔ c₁)
+TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
 TwoCat   {c₁}  {c₂} {ℓ} = record {
     Obj  = TwoObject  {c₁} ;
-    Hom = λ a b →   Two-Hom {c₁ } { ℓ}  a b   ; 
-    _o_ =  _×_  { c₁}  {ℓ} ;
+    Hom = λ a b →   Two-Hom {c₁ } { c₂}  a b   ; 
+    _o_ =  _×_  { c₁}  {c₂} ;
     _≈_ = λ a b →   hom a == hom b  ;
     Id  =  \{a} -> Two-id a ;
     isCategory  = record {
-            isEquivalence = record {refl = {!!} ; trans = {!!} ; sym = {!!} };
+            isEquivalence =  record {refl = *refl  {_} {_} {_} {{!!}}; trans = *trans  {_} {_} {_} {{!!}}; sym = *sym  {_} {_} {_} {{!!}}};
             identityL  = \{a b f} -> identityL {a} {b} {f} ;
             identityR  = \{a b f} -> identityR {a} {b} {f} ;
             o-resp-≈  = \{a b c f g h i} -> o-resp-≈  {a} {b} {c} {f} {g} {h} {i} ;
@@ -92,10 +94,8 @@
         associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → hom ( f × (g × h) ) == hom ( (f × g) × h )
         associative {_} {_} {_} {_} {f} {g} {h}  =   {!!}
 
-open import maybeCat  
-
-indexFunctor :  {c₁ c₂ ℓ : Level} ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {ℓ} ) (MaybeCat A )
-indexFunctor  {c₁} {c₂} {ℓ}  a b f g = record {
+indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {c₂} ) (MaybeCat A )
+indexFunctor  {c₁} {c₂} {ℓ} A  a b f g = record {
          FObj = λ a → fobj a
        ; FMap = λ f → fmap f
        ; isFunctor = record {
@@ -109,7 +109,7 @@
           fobj :  Obj I -> Obj A
           fobj t0 = a
           fobj t1 = b
-          fmap1 :  {x y : Obj I } ->  (Arrow  {ℓ} ) -> Hom MA (fobj x) (fobj y)
+          fmap1 :  {x y : Obj I } ->  (Arrow  {c₂} ) -> Hom MA (fobj x) (fobj y)
           fmap1 {t0} {t1} arrow-f = record { hom = just f }
           fmap1 {t0} {t1}  arrow-g = record { hom = just g }
           fmap1 {t0} {t0} id-t0  = record { hom = just ( id1 A a )}
@@ -144,11 +144,11 @@
 
 open Limit
 
-lim-to-equ : 
+lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ->
       (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 ) 
         → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g
-lim-to-equ  lim {a} {b} {c}  f g e fe=ge = record {
+lim-to-equ  {c₁} {c₂} {ℓ } A  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} → ek=h d h fh=gh