--- a/limit-to.agda	Sat Mar 04 16:57:58 2017 +0900
+++ b/limit-to.agda	Sun Mar 05 11:14:32 2017 +0900
@@ -66,37 +66,37 @@
                A [ fmap (T [ g o f ])  ≈  A [ fmap g o fmap f ] ]
           distr1  {t0} {t0} {t0} {id-t0 } { id-t0 } = let open  ≈-Reasoning A in sym-hom idL
           distr1  {t1} {t1} {t1} { id-t1 } { id-t1 } = let open  ≈-Reasoning A in begin
-                   id1 A b
+                   id b
                 ≈↑⟨ idL ⟩
-                   id1 A b o id1 A b
+                   id b o id b
                 ∎
           distr1  {t0} {t0} {t1} { id-t0 } { arrow-f } = let open  ≈-Reasoning A in begin
                   fmap (T [ arrow-f  o id-t0 ] )
                 ≈⟨⟩
                   fmap arrow-f
                 ≈↑⟨ idR ⟩
-                   fmap arrow-f o id1 A a
+                   fmap arrow-f o id a
                 ∎
           distr1  {t0} {t0} {t1}  { id-t0 } { arrow-g } = let open  ≈-Reasoning A in begin
                   fmap (T [ arrow-g  o id-t0 ] )
                 ≈⟨⟩
                   fmap arrow-g
                 ≈↑⟨ idR ⟩
-                   fmap arrow-g o id1 A a
+                   fmap arrow-g o id a
                 ∎
           distr1  {t0} {t1} {t1}  { arrow-f } { id-t1 } = let open  ≈-Reasoning A in begin
                   fmap (T [ id-t1  o arrow-f ] )
                 ≈⟨⟩
                   fmap arrow-f
                 ≈↑⟨ idL ⟩
-                   id1 A b o  fmap arrow-f
+                   id b o  fmap arrow-f
                 ∎
           distr1  {t0} {t1} {t1} { arrow-g } { id-t1 } = let open  ≈-Reasoning A in begin
                   fmap (T [ id-t1  o arrow-g ] )
                 ≈⟨⟩
                   fmap arrow-g
                 ≈↑⟨ idL ⟩
-                   id1 A b o  fmap arrow-g
+                   id b o  fmap arrow-g
                 ∎
 
 --- Nat for Limit
@@ -127,28 +127,28 @@
          commute1  {t0} {t1} {arrow-f}  d h fh=gh =  let open  ≈-Reasoning A in begin
                     f o h
                 ≈↑⟨ idR ⟩
-                    (f o h ) o id1 A d
+                    (f o h ) o id d
                 ∎
          commute1  {t0} {t1} {arrow-g}  d h fh=gh =  let open  ≈-Reasoning A in begin
                     g o h
                 ≈↑⟨ fh=gh ⟩
                     f o h
                 ≈↑⟨ idR ⟩
-                    (f o h ) o id1 A d
+                    (f o h ) o id d
                 ∎
          commute1  {t0} {t0} {id-t0}  d h fh=gh =   let open  ≈-Reasoning A in begin
-                    id1 A a o h
+                    id a o h
                 ≈⟨ idL ⟩
                     h
                 ≈↑⟨ idR ⟩
-                    h o id1 A d
+                    h o id d
                 ∎
          commute1  {t1} {t1} {id-t1}  d h fh=gh =   let open  ≈-Reasoning A in begin
-                    id1 A b o  ( f o  h  )
+                    id b o  ( f o  h  )
                 ≈⟨ idL ⟩
                      f o  h
                 ≈↑⟨ idR ⟩
-                    ( f o  h ) o id1 A d 
+                    ( f o  h ) o id d 
                 ∎
 
 
@@ -206,7 +206,7 @@
          uniq-nat {t1} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
                     TMap (limit-u comp Γ) t1 o k'
                 ≈↑⟨ car (idR) ⟩
-                    ( TMap (limit-u comp Γ) t1  o  id1 A c ) o k'
+                    ( TMap (limit-u comp Γ) t1  o  id c ) o k'
                 ≈⟨⟩
                     ( TMap (limit-u comp Γ) t1  o  FMap (K A I c) arrow-f ) o k'
                 ≈↑⟨ car ( nat1 (limit-u comp Γ) arrow-f ) ⟩