--- a/pullback.agda	Wed Sep 25 18:07:58 2013 +0900
+++ b/pullback.agda	Wed Sep 25 18:15:43 2013 +0900
@@ -473,18 +473,18 @@
          { η : NTrans A A identityFunctor ( U ○  F ) }
          { ε : NTrans B B  ( F ○  U ) identityFunctor } →
        ( adj : Adjunction A B U F η ε  ) →  Limit A I (U  ○ Γ) (FObj U lim) (ta1 B Γ lim tb limit U ) 
-adjoint-preseve-limit B Γ lim tb limit {U} {F} {η} {ε} adj = record {
+adjoint-preseve-limit B Γ lim tb limitb {U} {F} {η} {ε} adj = record {
      limit = λ a t → limit1 a t ;
      t0f=t = λ {a t i } → t0f=t1 {a} {t} {i}  ;
      limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
     } where
-         ta = ta1 B Γ lim tb limit U
+         ta = ta1 B Γ lim tb limitb U
          limit1 :  (a : Obj A) → NTrans I A (K A I a) (U  ○ Γ) → Hom A a (FObj U lim)
          limit1 a t = let  open ≈-Reasoning (A) in ?
          t0f=t1 :  {a : Obj A} {t : NTrans I A (K A I a) (U  ○ Γ)} {i : Obj I} →
                 A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ]
-         t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in ?
+         t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in {!!}
          limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K A I a) (U  ○ Γ)} {f : Hom A a (FObj U lim)} 
                 → ({i : Obj I} → A [ A [ TMap ta i o f ] ≈ TMap t i ]) →
                 A [ limit1 a t ≈ f ]
-         limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in ?
+         limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in {!!}