# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1380110595 -32400
# Node ID bba60d8434627ce100aa120c26a3fc0b906ad77a
# Parent  26e8f0227ebd1833b63e7da53895efc24f2a1dfc
lemma1 will be proved

diff -r 26e8f0227ebd -r bba60d843462 pullback.agda
--- a/pullback.agda	Wed Sep 25 20:24:39 2013 +0900
+++ b/pullback.agda	Wed Sep 25 21:03:15 2013 +0900
@@ -537,6 +537,7 @@
                ≈⟨ idL ⟩
                  TMap t i
                ∎
+         -- ta = TMap (Functor*Nat I A U tb) , FMap U ( TMap tb i )  o f  ≈ TMap t i
          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 ]
@@ -544,7 +545,19 @@
                  limit1 a t
                ≈⟨⟩
                  FMap U (limit limitb (FObj F a) (tF a t )) o TMap η a  
+               ≈⟨ car ( fcong U (limit-uniqueness limitb ( λ {i} →  lemma1 i) )) ⟩
+                 FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a  
                ≈⟨ {!!} ⟩
                  f
-               ∎
+               ∎ where
+                  lemma1 : (i : Obj I) → B [ B [ TMap tb i o B [ TMap ε lim  o FMap F f ] ] ≈ TMap (tF a t) i ]
+                  lemma1 i =  let  open ≈-Reasoning (B) in  begin
+                          TMap tb i o (TMap ε lim  o FMap F f)
+                       ≈⟨ {!!} ⟩
+                          TMap ε (FObj Γ i) o FMap F (TMap t i) 
+                       ≈⟨⟩
+                          TMap (tF a t) i  
+                       ∎ 
 
+     
+