Mercurial > hg > Members > kono > Proof > category

changeset 289:7dc163c026b7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
move to iProduct axiom
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 25 Sep 2013 13:25:14 +0900
parents 04f598e500de
children 1f897357ec6c
files pullback.agda
diffstat 1 files changed, 9 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Tue Sep 24 11:07:43 2013 +0900
+++ b/pullback.agda	Wed Sep 25 13:25:14 2013 +0900
@@ -318,6 +318,8 @@
    field
       product : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
       pif=q :   {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i )  o ( product qi ) ] ≈  (qi i) ]
+      -- special case of product ( qi = pi )
+      pif=q1 :   { i : I } → { qi :  Hom A p (ai i) } → A [ pi i ≈  qi ]
       ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
       ip-cong : {q : Obj A}   → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
                 → ( ∀ (i : I ) →  A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ]
@@ -351,9 +353,8 @@
      ( Γ : 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 fproj = record {
+limit-ε prod eqa Γ lim p e proj = record {
       TMap = tmap ;
       isNTrans = record {
           commute = commute1 
@@ -369,7 +370,7 @@
              FMap Γ f o ( proj i o e )
         ≈⟨ assoc ⟩
              ( FMap Γ f o  proj i ) o e 
-        ≈⟨ car fproj ⟩
+        ≈↑⟨ car ( pif=q1 ( prod p (FObj Γ)  proj ) {j} ) ⟩
              proj j o e 
         ≈↑⟨ idR ⟩
              (proj j o e ) o id1 A lim
@@ -384,10 +385,8 @@
      ( Γ : 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 )
-     --  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 I Γ lim ( limit-ε prod eqa Γ lim p e proj )
+limit-from prod eqa Γ lim p e proj = 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
@@ -395,9 +394,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 fproj ) i o limit1 a t ] ≈ TMap t i ]
+                A [ A [ TMap (limit-ε prod eqa Γ lim p e proj ) 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 fproj ) i o limit1 a t 
+                   TMap (limit-ε prod eqa Γ lim p e proj ) 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  ⟩
@@ -408,7 +407,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 fproj ) i o f ] ≈ TMap t i ]) →
+                → ({i : Obj I} → A [ A [ TMap (limit-ε prod eqa Γ lim p e proj ) 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