Mercurial > hg > Members > kono > Proof > category

changeset 303:7f40d6a51c72

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Limit form equalizer and product done. Use equalizer to provle naturality of limit-ε
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 04 Nov 2013 14:46:07 +0900
parents c5b2656dbec6
children bd7b3f3d1d4c
files pullback.agda
diffstat 1 files changed, 23 insertions(+), 48 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Wed Oct 30 19:35:14 2013 +0900
+++ b/pullback.agda	Mon Nov 04 14:46:07 2013 +0900
@@ -314,6 +314,18 @@
             f
         ∎
 
+
+lemma-p0 :   (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : Product A a b ab π1 π2 ) →
+      A [ _×_ prod π1 π2 ≈  id1 A ab  ]
+lemma-p0  a b ab π1 π2 prod =  let  open ≈-Reasoning (A) in begin
+             _×_ prod π1 π2
+         ≈↑⟨ ×-cong prod idR idR ⟩
+             _×_ prod (A [ π1 o id1 A ab ]) (A [ π2 o id1 A ab ])
+         ≈⟨ Product.uniqueness prod ⟩
+             id1 A ab 
+         ∎
+
+
 -----
 --
 -- product on arbitrary index
@@ -327,17 +339,14 @@
    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 ) ( should b proved from pif=q )
-      --   we cannot prove this because qi/pi cannot be interleaved , should be the way to prove
-      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' ]
    -- another form of uniquness
-   ip-uniquness1 : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) 
+   ip-uniqueness1 : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) 
           → ( ∀ { i : I } →  A [ A [ ( pi i )  o product' ] ≈  (qi i) ] )
           → A [ product'  ≈ product qi ]
-   ip-uniquness1 {a} qi product' eq =  let  open ≈-Reasoning (A) in begin
+   ip-uniqueness1 {a} qi product' eq =  let  open ≈-Reasoning (A) in begin
            product'
          ≈↑⟨ ip-uniqueness ⟩
            product (λ i₁ → A [ pi i₁ o product' ])
@@ -348,20 +357,6 @@
          ∎ ) ⟩
            product qi
          ∎ 
-   pif=q1' :   { i : I } → { qi : (j : I ) →  Hom A p (ai j) } → A [ pi i ≈  qi i ]
-   pif=q1' {i} {qi} = let  open ≈-Reasoning (A) in begin
-           pi i
-         ≈↑⟨ idR ⟩
-           pi i o id1 A p
-         ≈⟨ cdr ( ip-uniquness1 {p} qi (id1 A p) ( begin
-           pi ? o id1 A p
-         ≈⟨ {!!} ⟩
-           qi ?
-         ∎ )) ⟩
-           pi i o product qi
-         ≈⟨ pif=q {p} qi {i} ⟩
-           qi i
-         ∎ 
 
 open IProduct
 open Equalizer
@@ -375,7 +370,7 @@
 --        | pi                          lim = K i -----------→ K j = lim
 --        |                                     |               |
 --        p                                     |               |
---        ^                                 ε i |               | ε j
+--        ^                    proj i o e = ε i |               | ε j = proj j o e
 --        |                                     |               |
 --        | e = equalizer (id p) (id p)         |               |
 --        |                                     v               v
@@ -383,35 +378,15 @@
 --         k ( product pi )                          Γ f
 --                                              Γ f o ε i = ε j 
 --
---
-
--- pi-ε -- : ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
---                   →  IProduct {c₁'} A (Obj I) p ai pi )
---      ( lim p : Obj A ) ( e : Hom  A lim p )
---      ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
---      { i : Obj I } → { q :  ( i : Obj I )  → Hom A p (FObj Γ i) } → A [ proj i ≈  q i ]
--- pi-ε prod lim p e proj {i} {q} = let  open ≈-Reasoning (A) in begin
---            proj i 
---         ≈↑⟨ idR ⟩
---            proj i o id1 A p
---         ≈⟨ cdr {!!} ⟩
---            proj i o product (prod p (FObj Γ) proj) q
---         ≈⟨ pif=q (prod p (FObj Γ) proj)  q ⟩
---            q i
---         ∎
-
 
 limit-ε :
-      ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
-                  →  IProduct {c₁'} A (Obj I) p ai pi )
+     ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → Equalizer A e f g )
      ( lim p : Obj A ) ( e : Hom  A lim p )
      ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
          NTrans I A (K A I lim) Γ
-limit-ε prod lim p e proj = record {
+limit-ε eqa lim p e proj = record {
       TMap = tmap ;
-      isNTrans = record {
-          commute = commute1 
-      }
+      isNTrans = record { commute = commute1 }
   } where
       tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i)
       tmap i = A [ proj i o e ]
@@ -423,7 +398,7 @@
              FMap Γ f o ( proj i o e )
         ≈⟨ assoc ⟩
              ( FMap Γ f o  proj i ) o e 
-        ≈↑⟨ car ( pif=q1 ( prod p (FObj Γ)  proj ) {j} ) ⟩
+        ≈⟨ fe=ge ( eqa e (FMap Γ f o  proj i) ( proj j ))  ⟩
              proj j o e 
         ≈↑⟨ idR ⟩
              (proj j o e ) o id1 A lim
@@ -438,7 +413,7 @@
      ( 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 A I Γ lim ( limit-ε prod lim p e proj )
+      → Limit A I Γ lim ( limit-ε 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}  ;
@@ -447,9 +422,9 @@
          limit1 :  (a : Obj A) → NTrans I A (K A 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 A I a) Γ} {i : Obj I} →
-                A [ A [ TMap (limit-ε prod lim p e proj ) i o limit1 a t ] ≈ TMap t i ]
+                A [ A [ TMap (limit-ε 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 lim p e proj ) i o limit1 a t 
+                   TMap (limit-ε 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  ⟩
@@ -460,7 +435,7 @@
                    TMap t i 
                 ∎
          limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim} 
-                → ({i : Obj I} → A [ A [ TMap (limit-ε prod lim p e proj ) i o f ] ≈ TMap t i ]) →
+                → ({i : Obj I} → A [ A [ TMap (limit-ε 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