# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1380105250 -32400
# Node ID fb0ab8c72e15476851090a81786b2d177823abbc
# Parent  a84fab7cf46abe81d2223885679cca3eba7295a2
limit defined.

diff -r a84fab7cf46a -r fb0ab8c72e15 pullback.agda
--- a/pullback.agda	Wed Sep 25 18:15:43 2013 +0900
+++ b/pullback.agda	Wed Sep 25 19:34:10 2013 +0900
@@ -470,21 +470,32 @@
      { c₁' c₂' ℓ' : Level}  (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) 
      ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limit : Limit B I Γ lim tb ) →
          { U : Functor B A } { F : Functor A B }
-         { η : NTrans A A identityFunctor ( U ○  F ) }
+         { η : 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 ) 
+       ( 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 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 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} →
+         tfmap : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → (i : Obj I) → Hom B (FObj (K B I (FObj F a)) i) (FObj Γ i)
+         tfmap a t i  = B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ]
+         tF :  (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) →  NTrans I B (K B I (FObj F a)) Γ
+         tF a t = record {
+             TMap = tfmap a t ; 
+             isNTrans = record { commute = λ {a'} {b} {f} → let  open ≈-Reasoning (B) in begin
+                  FMap Γ f o tfmap a t a' 
+               ≈⟨ {!!}  ⟩
+                  tfmap a t b o FMap (K B I (FObj F a)) f 
+               ∎
+          } }
+         limit1 :  (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U lim)
+         limit1 a t = A [ FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a ]
+         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 {!!}
-         limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K A I a) (U  ○ Γ)} {f : Hom A a (FObj U lim)} 
+         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 {!!}