Mercurial > hg > Members > kono > Proof > category

changeset 288:04f598e500de

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
give up ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 24 Sep 2013 11:07:43 +0900
parents a0455048ebb7
children 7dc163c026b7
files pullback.agda
diffstat 1 files changed, 11 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Tue Sep 24 00:47:33 2013 +0900
+++ b/pullback.agda	Tue Sep 24 11:07:43 2013 +0900
@@ -351,8 +351,9 @@
      ( Γ : Functor I A ) →
      ( lim p : Obj A ) ( e : Hom  A lim p )
      ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
+     ( fproj : { i j : Obj I } { f : Hom I i j } → A [ A [ FMap Γ f o proj i ] ≈  proj j  ]  )  →
          NTrans I A (K I lim) Γ
-limit-ε prod eqa Γ lim p e proj = record {
+limit-ε prod eqa Γ lim p e proj fproj = record {
       TMap = tmap ;
       isNTrans = record {
           commute = commute1 
@@ -368,25 +369,13 @@
              FMap Γ f o ( proj i o e )
         ≈⟨ assoc ⟩
              ( FMap Γ f o  proj i ) o e 
-        ≈↑⟨ 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 
-        ≈⟨ car ( cdr ( ip-uniqueness ( prod p (FObj Γ) proj ))) ⟩
-             (proj j o  id1 A p  ) o e 
-        ≈⟨ car idR ⟩
+        ≈⟨ car fproj ⟩
              proj j o e 
         ≈↑⟨ idR ⟩
              (proj j o e ) o id1 A lim
         ≈⟨⟩
              tmap j o FMap (K I lim) f
-        ∎ where
-           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 ) )
@@ -395,8 +384,10 @@
      ( Γ : Functor I A ) → ( lim p : Obj A )       -- limit to be made
      ( e : Hom  A lim p )                          -- existing of equalizer
      ( proj : (i : Obj I ) → Hom A p (FObj Γ i) )  -- existing of product ( projection actually )
-      → Limit I Γ lim ( limit-ε prod eqa Γ lim p e proj )
-limit-from prod eqa Γ lim p e proj = record {
+     --  fproj should be proved by IProduct, but I cannot
+     ( fproj : { i j : Obj I } { f : Hom I i j } → A [ A [ FMap Γ f o proj i ] ≈  proj j  ]  )  
+      → Limit I Γ lim ( limit-ε prod eqa Γ lim p e proj fproj )
+limit-from prod eqa Γ lim p e proj fproj = 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
@@ -404,9 +395,9 @@
          limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a lim
          limit1 a t = let  open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom
          t0f=t1 :  {a : Obj A} {t : NTrans I A (K I a) Γ} {i : Obj I} →
-                A [ A [ TMap (limit-ε prod eqa Γ lim p e proj) i o limit1 a t ] ≈ TMap t i ]
+                A [ A [ TMap (limit-ε prod eqa Γ lim p e proj fproj ) i o limit1 a t ] ≈ TMap t i ]
          t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in begin
-                   TMap (limit-ε prod eqa Γ lim p e proj) i o limit1 a t 
+                   TMap (limit-ε prod eqa Γ lim p e proj fproj ) i o limit1 a t 
                 ≈⟨⟩
                    ( ( proj i )  o e ) o  k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom
                 ≈↑⟨ assoc  ⟩
@@ -417,7 +408,7 @@
                    TMap t i 
                 ∎
          limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K I a) Γ} {f : Hom A a lim} 
-                → ({i : Obj I} → A [ A [ TMap (limit-ε prod eqa Γ lim p e proj) i o f ] ≈ TMap t i ]) →
+                → ({i : Obj I} → A [ A [ TMap (limit-ε prod eqa Γ lim p e proj fproj ) i o f ] ≈ TMap t i ]) →
                 A [ limit1 a t ≈ f ]
          limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in begin
                     limit1 a t