Mercurial > hg > Members > kono > Proof > category

changeset 286:981253b05b0b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
uum
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 24 Sep 2013 00:29:05 +0900
parents 46d4ad55b948
children a0455048ebb7
files pullback.agda
diffstat 1 files changed, 8 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- 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 :