--- a/pullback.agda	Sun Sep 22 11:08:41 2013 +0900
+++ b/pullback.agda	Sun Sep 22 13:19:01 2013 +0900
@@ -6,7 +6,7 @@
 
 open import Category -- https://github.com/konn/category-agda
 open import Level
-module pullback { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
+module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where
 
 open import HomReasoning
 open import cat-utility
@@ -126,8 +126,16 @@
                  p'
              ∎
 
-K : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) → ( a : Obj A ) → Functor I A
-K I Γ a = record {
+------
+--
+-- Limit
+--
+-----
+
+-- Constancy Functor
+
+K : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → ( 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 {
@@ -140,11 +148,63 @@
 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
+     ( 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 } →
+     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 } →
+     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 ]
 
+--------------------------------
+--
+-- If we have two limits on c and c', there are isomorphic pair h, h'
+
+open Limit
+
+iso-l :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
+     ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) (  t0' : NTrans I A ( K I a0' ) Γ )
+       ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' ) 
+      → Hom A a0 a0'
+iso-l  I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0
+
+iso-r :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
+     ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) (  t0' : NTrans I A ( K I a0' ) Γ )
+       ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' ) 
+      → Hom A a0' a0
+iso-r  I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0'
+
+
+iso-lr :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
+     ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) (  t0' : NTrans I A ( K I a0' ) Γ )
+       ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' )  → ∀{ i : Obj I } →
+  A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim'  ]  ≈ id1 A a0' ]
+iso-lr  I Γ a0 a0' t0 t0' lim lim' {i} =  let open ≈-Reasoning (A) in begin
+           limit lim' a0 t0 o limit lim a0' t0'
+      ≈↑⟨ limit-uniqueness lim' i ( begin
+          TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' )
+      ≈⟨ assoc  ⟩
+          ( TMap t0' i o  limit lim' a0 t0 ) o limit lim a0' t0' 
+      ≈⟨ car ( t0f=t lim' ) ⟩
+          TMap t0 i o limit lim a0' t0' 
+      ≈⟨ t0f=t lim ⟩
+          TMap t0' i 
+      ∎ ) ⟩
+           limit lim' a0' t0'
+      ≈⟨ limit-uniqueness lim' i idR ⟩
+           id a0'
+      ∎
+
+
+open import CatExponetial I A
+
+KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) → ( a : Obj A ) → Functor I A
+KI 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
+        }
+  }