--- a/limit-to.agda	Tue Mar 14 12:14:57 2017 +0900
+++ b/limit-to.agda	Tue Mar 14 13:08:03 2017 +0900
@@ -226,7 +226,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 (isLimit lim) k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
+                ≈⟨ limit-uniqueness (isLimit lim) ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
                     k'
                 ∎
 
@@ -290,7 +290,7 @@
         ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (limit-u comp Γ) i o h ] ≈ A [ pi i o h ] ]
         ipu {i} q h = let open  ≈-Reasoning A in  refl-hom
         ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
-        ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i  o h ]  )} h (ipu q h)
+        ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i  o h ]  )} (ipu q h)
         ipc : {q : Obj A}   → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } 
              → (i : I ) →  A [ qi i ≈ qi' i ]  → 
              A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ]
@@ -309,4 +309,4 @@
                 ∎
         ip-cong : {q : Obj A}   → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
                         → ( ∀ (i : I ) →  A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ]
-        ip-cong {q} {qi} {qi'} qi=qi' =  limit-uniqueness (isLimit lim) {q} {pnat A S Γ qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))
+        ip-cong {q} {qi} {qi'} qi=qi' =  limit-uniqueness (isLimit lim) {q} {pnat A S Γ qi}  (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))