# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1379950145 -32400
# Node ID 981253b05b0b6b2d3de058e517595f081b20b6d3
# Parent  46d4ad55b948f73844c32e4ab1d2e9d5f737efc1
uum

diff -r 46d4ad55b948 -r 981253b05b0b pullback.agda
--- a/pullback.agda	Mon Sep 23 20:54:30 2013 +0900
+++ b/pullback.agda	Tue Sep 24 00:29:05 2013 +0900
@@ -368,9 +368,9 @@
              FMap Γ f o ( proj i o e )
         ≈⟨ assoc ⟩
              ( FMap Γ f o  proj i ) o e 
-        ≈↑⟨ car ( pif=q ( prod p (FObj Γ) proj ) {!!} )  ⟩
-              {!!}
-        ≈⟨ {!!} ⟩
+        ≈↑⟨ car ( pif=q ( prod p (FObj Γ) lemma1 ) lemma2 {j} )  ⟩
+             (proj j o ( product ( prod p (FObj Γ) lemma1 ) )  lemma2 ) o e 
+        ≈⟨ car ( cdr ( ip-cong ( prod p (FObj Γ) proj ) {!!} )) ⟩
              (proj j o ( product ( prod p (FObj Γ) proj ) ) proj  ) o e 
         ≈⟨ car ( cdr ( ip-cong ( prod p (FObj Γ) proj ) (λ i₁ → sym idR ) )) ⟩
              (proj j o ( product ( prod p (FObj Γ) proj ) ) (λ i₁ → A [ proj i₁ o id1 A p ]) ) o e 
@@ -382,7 +382,11 @@
              (proj j o e ) o id1 A lim
         ≈⟨⟩
              tmap j o FMap (K I lim) f
-        ∎ 
+        ∎ where
+           lemma1 : (i₁ : Obj I) → Hom A p (FObj Γ i₁) 
+           lemma1 i₁ = {!!}
+           lemma2 : (i₁ : Obj I) → Hom A p (FObj Γ i₁) 
+           lemma2 i₁ = {!!}
 
 
 limit-from :