--- a/discrete.agda	Thu Mar 02 14:58:40 2017 +0900
+++ b/discrete.agda	Thu Mar 02 17:41:20 2017 +0900
@@ -204,7 +204,7 @@
 
 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 A f g comp = {!!}
+equlimit {c₁} {c₂} {ℓ} A {a} {b} f g comp = ? -- TMap (limit-u comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) t0
 
 lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
       (comp : Complete A (TwoCat {c₁} {c₂} ) )
@@ -220,16 +220,86 @@
          I = TwoCat {c₁} {c₂}
          Γ : Functor I A
          Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g
-         eqlim = isLimit comp Γ
          c = limit-c comp Γ
-         e = equlimit A f g comp
          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  = {!!}
+         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 ] ]
+                 → 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 with f'
+         commute1  {t0} {t1} {f'}  d h fh=gh | arrow-f =  let open  ≈-Reasoning A in begin
+                    f o h
+                ≈↑⟨ idR ⟩
+                    (f o h ) o id1 A d
+                ∎
+         commute1  {t0} {t1} {f'}  d h fh=gh | arrow-g =  let open  ≈-Reasoning A in begin
+                    g o h
+                ≈↑⟨ fh=gh ⟩
+                    f o h
+                ≈↑⟨ idR ⟩
+                    (f o h ) o id1 A d
+                ∎
+         commute1  {t0} {t0} {f'}  d h fh=gh | id-t0 =   let open  ≈-Reasoning A in begin
+                    id1 A a o h
+                ≈⟨ idL ⟩
+                    h
+                ≈↑⟨ idR ⟩
+                    h o id1 A d
+                ∎
+         commute1  {t1} {t1} {f'}  d h fh=gh | id-t1 =   let open  ≈-Reasoning A in begin
+                    id1 A b o  ( f o  h  )
+                ≈⟨ idL ⟩
+                     f o  h
+                ≈↑⟨ idR ⟩
+                    ( f o  h ) o id1 A d 
+                ∎
+         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 
+            }
+          }
+         e =  equlimit A f g comp
+         eqlim =  isLimit comp  Γ (nat1 c e fe=ge )
+         k {d} h fh=gh  =  limit eqlim 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 = {!!} 
-         uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ {!!} o k' ] ≈ {!!} ]
-         uniq-nat  = {!!}
-         uniquness :  (d : Obj A ) (h : Hom A d a ) →  ?　→ -- ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  →
+         ek=h d h fh=gh = let open  ≈-Reasoning A in  begin
+                    e o k h fh=gh
+                ≈⟨ t0f=t eqlim {d} {nat1 d h fh=gh} {t0}  ⟩
+                    h
+                ∎
+         uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c ) 
+                       ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ]) → A [ A [ e o k' ] ≈ h ] →  
+                       A [ A [ TMap (nat1 c e fe=ge ) i o k' ] ≈ TMap (nat1 d h fh=gh) i ]
+         uniq-nat {t0} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
+                    (nmap t0 c e ) o k'
+                ≈⟨⟩
+                    e o k'
+                ≈⟨ ek'=h ⟩
+                    h
+                ≈⟨⟩
+                    nmap t0 d h
+                ∎
+         uniq-nat {t1} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
+                   (nmap t1 c e ) o k'
+                ≈⟨⟩
+                   (f o e ) o k'
+                ≈↑⟨ assoc ⟩
+                   f o ( e o k' )
+                ≈⟨ cdr  ek'=h ⟩
+                    f o h
+                ≈⟨⟩
+                    TMap (nat1 d h fh=gh) t1
+                ∎
+         uniquness :  (d : Obj A ) (h : Hom A d a ) →  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  →
                  ( k' : Hom A d c )
-                → A [ A [ e o k' ] ≈ h ] → A [ k h {!!} ≈ k' ]
-         uniquness = {!!}
+                → 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 ) ⟩
+                    k'
+                ∎
+