--- a/limit-to.agda	Sat Mar 26 12:31:14 2016 +0900
+++ b/limit-to.agda	Sat Mar 26 13:50:18 2016 +0900
@@ -445,24 +445,66 @@
         ; 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
+         open  ≈-Reasoning A
          I = I'   {c₁} {c₂} {ℓ} 
          Γ = indexFunctor  {c₁} {c₂} {ℓ} A  none 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)
          nmap x d h with x 
          ... | t0 = h
          ... | t1 =  A [ f o  h ] 
-         commute1 : {x y : Obj I}  {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ]
+         commute1 : {x y : Obj I}  {f' : Hom I x y} { ar : Maybe ( Arrow  {c₁} {c₂} t0 t1 x y ) } 
+              (d : Obj A) (h : Hom A d a ) ->  A [ A [ f  o  h ] ≈ A [ g  o h ] ]
                  → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
-         commute1  {x} {y} {f'} d h fh=gh = {!!}
-         nat : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans I A (K A I d) Γ
-         nat d h fh=gh = record {
+         commute1  {t0} {t0} {f'} { nothing } d h fh=gh = begin
+                    FMap Γ f' o nmap t0 d h 
+                ≈⟨⟩
+                   nil {!!}  o h 
+                ≈⟨ nil-idL {!!} ⟩
+                    h 
+                ≈↑⟨ idR  ⟩
+                    h o id1 A d
+                ≈⟨⟩
+                    nmap t0 d h o id1 A d
+                ≈⟨⟩
+                    nmap t0 d h o FMap (K A I d) f'
+                ∎
+         commute1  {t0} {t1} {f'} { nothing } d h fh=gh = {!!}
+         commute1  {t1} {t0} {f'} { nothing } d h fh=gh = {!!}
+         commute1  {t1} {t1} {f'} { nothing } d h fh=gh = {!!}
+         commute1  {t1} {t0} {f'} { just inv-f } d h fh=gh = {!!}
+         commute1  {t0} {t1} {f'} { just arrow-f } d h fh=gh =  begin
+                    FMap Γ f' o nmap t0 d h
+                ≈⟨⟩
+                    {!!} o h
+                ≈⟨ {!!} ⟩
+                     f o  h 
+                ≈↑⟨ idR  ⟩
+                    ( f o  h ) o  id1 A d
+                ≈⟨⟩
+                    nmap t1 d h o FMap (K A I d) f'
+                ∎
+         commute1  {t0} {t1} {f'} { just arrow-g } d h fh=gh =  begin
+                    FMap Γ f' o nmap t0 d h
+                ≈⟨⟩
+                    ? o h
+                ≈⟨ {!!} ⟩
+                     f o  h
+                ≈↑⟨ idR  ⟩
+                    ( f o  h ) o  id1 A d
+                ≈⟨⟩
+                    nmap t1 d h o FMap (K A I d) f'
+                ∎
+         commute1  {t0} {t0} {f'} { just id-t0 } d h fh=gh = {!!}
+         commute1  {t1} {t1} {f'} { just id-t1 } d h fh=gh = {!!}
+         nat1 : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans I A (K A I d) Γ
+         nat1 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
+                commute = λ {x} {y} {f'} -> commute1 {x} {y} {f'} { hom f' } d h fh=gh 
             }
           }
          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 e fe=ge }) d (nat d h fh=gh ) 
+         k {d} h fh=gh  = limit (lim Γ  {c} {nat1 c e fe=ge }) d (nat1 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 = {!!}
          uniquness :  (d : Obj A ) (h : Hom A d a ) ->  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  ->