Mercurial > hg > Members > kono > Proof > category

changeset 283:5492a0681f55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Sep 2013 19:08:23 +0900
parents c831abfa9bf4
children 4be696e3fd94
files pullback.agda
diffstat 1 files changed, 51 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Mon Sep 23 17:23:40 2013 +0900
+++ b/pullback.agda	Mon Sep 23 19:08:23 2013 +0900
@@ -319,30 +319,32 @@
       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) ]
       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) )
+      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' ]
 
 open IProduct
+open Equalizer
 
 --
 -- limit from equalizer and product
 --
 --      
---       ai 
---      ^ ^
---      | | pi
---      | |
---      | p 
---      | ^ 
---      | |
---      | | e = equalizer (f pi) (g pi')
---      | |
---       lim <------------------ d'
---         k ( product pi )
+--        ai 
+--        ^                                       K f = id lim
+--        | pi                          lim = K i ------------> K j = lim
+--        |                                     |               |
+--        p                                     |               |
+--        ^                                 ε i |               | ε j
+--        |                                     |               |
+--        | e = equalizer (f pi) (g pi')        |               |
+--        |                                     v               v
+--       lim <------------------ d'     a i = Γ i ------------> Γ j = a j
+--         k ( product pi )                          Γ f
+--                                              Γ f o ε i = ε j 
+--
+--
 
-open Equalizer
-
-limit-equalizer :
+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 )
@@ -350,7 +352,7 @@
      ( lim p : Obj A ) ( e : Hom  A lim p )
      ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
          NTrans I A (K I lim) Γ
-limit-equalizer prod eqa Γ lim p e proj = record {
+limit-ε prod eqa Γ lim p e proj = record {
       TMap = tmap ;
       isNTrans = record {
           commute = commute1 
@@ -358,21 +360,9 @@
   } where
       tmap : (i : Obj I) → Hom A (FObj (K I lim) i) (FObj Γ i)
       tmap i = A [ ( proj i )  o e ]
-      commute1 :  {a b : Obj I} {f : Hom I a b} →
-        A [ A [ FMap Γ f o tmap a ] ≈ A [ tmap b o FMap (K I lim) f ] ]
-      commute1 {i} {j} {f} = let  open ≈-Reasoning (A) in begin
-             FMap Γ f o tmap i
-        ≈⟨⟩
-             FMap Γ f o ( proj i o e )
-        ≈⟨ assoc ⟩
-             ( FMap Γ f o  proj i ) o e 
-        ≈⟨ {!!} ⟩
-             proj j o e 
-        ≈↑⟨ idR ⟩
-             (proj j o e ) o id1 A lim
-        ≈⟨⟩
-             tmap j o FMap (K I lim) f
-        ∎
+      commute1 :  {i j : Obj I} {f : Hom I i j} →
+        A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K I lim) f ] ]
+      commute1 {i} {j} {f} = {!!}
 
 limit-from :
       ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
@@ -381,18 +371,41 @@
      ( Γ : Functor I A ) →
      ( lim p : Obj A ) ( e : Hom  A lim p )
      ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
-        Limit I Γ lim ( limit-equalizer prod eqa Γ lim p e proj )
+        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
     }  where
          limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a lim
-         limit1 a t = k (eqa e {!!} {!!} ) (product ( prod p (FObj Γ)  proj ) (TMap t) ) {!!}
+         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-equalizer prod eqa Γ lim p e proj) i o limit1 a t ] ≈ TMap t i ]
-         t0f=t1 = {!!}  
-         limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K I a) Γ} {f : Hom A a lim} → ({i : Obj I} →
-                A [ A [ TMap (limit-equalizer prod eqa Γ lim p e proj) i o f ] ≈ 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) 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  ⟩
+                    proj i  o ( e  o  k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom )
+                ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩
+                    proj i  o product (prod p (FObj Γ) proj) (TMap t)
+                ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩
+                   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 ]) →
                 A [ limit1 a t ≈ f ]
-         limit-uniqueness1 = {!!}
+         limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in begin
+                    limit1 a t
+                ≈⟨⟩
+                    k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom
+                ≈⟨ Equalizer.uniqueness  (eqa e (id1 A p) (id1 A p )) ( begin
+                      e o f 
+                ≈↑⟨ ip-uniqueness (prod p (FObj Γ) proj) ⟩
+                      product (prod p (FObj Γ) proj) (λ i → ( proj i o ( e  o f ) ) )
+                ≈⟨ ? ⟩
+                      product (prod p (FObj Γ) proj) (TMap t)
+                ∎ ) ⟩
+                    f
+                ∎
+