# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1379815721 -32400
# Node ID 367e8fde93ee1d18f9cbc4b0cc82a9823ae6a78a
# Parent  78ce12f8e6b613c84fe6b8672189ff133ff43415
add limit

diff -r 78ce12f8e6b6 -r 367e8fde93ee cat-utility.agda
--- a/cat-utility.agda	Fri Sep 20 21:21:48 2013 +0900
+++ b/cat-utility.agda	Sun Sep 22 11:08:41 2013 +0900
@@ -172,8 +172,11 @@
               ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ] 
            axb : Obj A
            axb = ab
+           pi1 : Hom A ab a 
+           pi1  = π1 
+           pi2 : Hom A ab b 
+           pi2  = π2 
 
-        -- 
         -- Pullback
         --         f
         --     a -------> c
@@ -202,3 +205,7 @@
                      →  A [ p eq  ≈ p' ]
            axb : Obj A
            axb = ab
+           pi1 : Hom A ab a 
+           pi1  = π1 
+           pi2 : Hom A ab b 
+           pi2  = π2 
diff -r 78ce12f8e6b6 -r 367e8fde93ee pullback.agda
--- a/pullback.agda	Fri Sep 20 21:21:48 2013 +0900
+++ b/pullback.agda	Sun Sep 22 11:08:41 2013 +0900
@@ -126,3 +126,25 @@
                  p'
              ∎
 
+K : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) → ( a : Obj A ) → Functor I A
+K 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
+        }
+  }
+
+open NTrans
+
+record Limit { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) 
+     ( a0 : Obj A ) (  t0 : NTrans I A ( K I Γ a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
+  field
+     limit :  ( a : Obj A ) → ( t : NTrans I A ( K I Γ a ) Γ ) → Hom A a a0
+     t0f=t :  { a : Obj A } → { t : NTrans I A ( K 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 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 ]
+