Mercurial > hg > Members > kono > Proof > category
changeset 287:a0455048ebb7
ion going
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 24 Sep 2013 00:47:33 +0900 |
| parents | 981253b05b0b |
| children | 04f598e500de |
| files | pullback.agda |
| diffstat | 1 files changed, 5 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/pullback.agda Tue Sep 24 00:29:05 2013 +0900 +++ b/pullback.agda Tue Sep 24 00:47:33 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 Γ) lemma1 ) lemma2 {j} ) ⟩ - (proj j o ( product ( prod p (FObj Γ) lemma1 ) ) lemma2 ) o e - ≈⟨ car ( cdr ( ip-cong ( prod p (FObj Γ) proj ) {!!} )) ⟩ + ≈↑⟨ car ( pif=q ( prod p (FObj Γ) proj ) { p } lemma2 {j} ) ⟩ + (proj j o ( product ( prod p (FObj Γ) proj ) ) lemma2 ) o e + ≈⟨ car ( cdr ( ip-cong ( prod p (FObj Γ) proj ) lemma3 )) ⟩ (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 @@ -383,11 +383,10 @@ ≈⟨⟩ 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₁ = {!!} - + lemma3 : (i₁ : Obj I) → A [ lemma2 i₁ ≈ proj i₁ ] + lemma3 = {!!} limit-from : ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) )