# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489547424 -32400
# Node ID c981a2f0642f2c3ef1d1e8f17a67135bd61202a3
# Parent  e8b85a05a6b29503e244682b014dd183c0ecdc34
UpreseveLimit detailing

diff -r e8b85a05a6b2 -r c981a2f0642f freyd2.agda
--- a/freyd2.agda	Wed Mar 15 11:19:54 2017 +0900
+++ b/freyd2.agda	Wed Mar 15 12:10:24 2017 +0900
@@ -33,6 +33,9 @@
 
 open NTrans 
 open Functor
+open Limit
+open IsLimit
+open import Category.Cat
 
 HomA : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂})
 HomA  {c₁} {c₂} {ℓ} A  a = record {
@@ -79,4 +82,22 @@
 UpreseveLimit : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → ( U : Functor A (Sets {c₂}) ) (b : Obj A)
       { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' )
      ( rep :  Representable A U b ) → LimitPreserve A I (Sets  {c₂}) U 
-UpreseveLimit  = {!!}
+UpreseveLimit {_} { c₂} A U b I rep =  record {
+       preserve = λ Γ limita → record {
+             limit = λ a t → limitu a Γ t limita
+             ; t0f=t = λ { a  t i }  → t0f=tu {a} Γ t limita {i}
+             ; limit-uniqueness = λ { a t f } t=f  → limit-uniquenessu {a} Γ limita t  f t=f
+       }
+   } where
+      limitu :   ( a : Obj (Sets  {c₂}) ) → (Γ : Functor I A )  ( t :  NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →   ( limita : Limit A I Γ  ) →   Hom Sets a (FObj U (a0 limita))
+      limitu  = {!!}
+      t0f=tu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) →  ( limita : Limit A I Γ  ) → 
+           ∀ { i : Obj I } →  Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o limitu a Γ t limita ] ≈ TMap t i ]
+      t0f=tu  = {!!}
+      limit-uniquenessu :    { a : Obj  (Sets  {c₂}) } → (Γ : Functor I A ) 
+           →   ( limita : Limit A I Γ  ) →
+          ( t : NTrans I Sets ( K Sets I a ) (U ○ Γ) ) → ( f :  Hom Sets a (FObj U (a0 limita)) ) 
+           →  (  ∀ { i : Obj I } →  (Sets [ TMap (LimitNat A I Sets Γ (a0 limita) (t0 limita) U) i o f ] ≡ TMap t i ) )
+           →  Sets [ limitu a Γ t limita ≈ f ]
+      limit-uniquenessu = {!!}
+