--- a/cat-utility.agda	Sun Jan 05 19:34:11 2014 +0900
+++ b/cat-utility.agda	Sun Jan 05 23:37:12 2014 +0900
@@ -231,3 +231,37 @@
            pi1  = π1 
            pi2 : Hom A ab b 
            pi2  = π2 
+
+        --
+        -- Limit
+        --
+        -----
+
+        -- Constancy Functor
+
+        K : { c₁' c₂' ℓ' : Level}  (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) 
+            → ( a : Obj A ) → Functor I A
+        K A I a = record {
+              FObj = λ i → a ;
+              FMap = λ f → id1 A a ;
+                isFunctor = let  open ≈-Reasoning (A) in record {
+                       ≈-cong   = λ f=g → refl-hom
+                     ; identity = refl-hom
+                     ; distr    = sym idL
+                }
+          }
+
+
+        record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
+             ( a0 : Obj A ) (  t0 : NTrans I A ( K A I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
+          field
+             limit :  ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0
+             t0f=t :  { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } →
+                 A [ A [ TMap t0 i o  limit a t ]  ≈ TMap t i ]
+             limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
+                 A [ A [ TMap t0 i o  f ]  ≈ TMap t i ] ) → A [ limit a t ≈ f ]
+          A0 : Obj A
+          A0 = a0
+          T0 : NTrans I A ( K A I a0 ) Γ
+          T0 = t0
+