Mercurial > hg > Members > kono > Proof > category

changeset 285:46d4ad55b948

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
commutativity continue...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Sep 2013 20:54:30 +0900
parents 4be696e3fd94
children 981253b05b0b
files pullback.agda
diffstat 1 files changed, 34 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Mon Sep 23 19:12:45 2013 +0900
+++ b/pullback.agda	Mon Sep 23 20:54:30 2013 +0900
@@ -336,7 +336,7 @@
 --        p                                     |               |
 --        ^                                 ε i |               | ε j
 --        |                                     |               |
---        | e = equalizer (f pi) (g pi')        |               |
+--        | e = equalizer (id p) (id p)         |               |
 --        |                                     v               v
 --       lim <------------------ d'     a i = Γ i ------------> Γ j = a j
 --         k ( product pi )                          Γ f
@@ -359,19 +359,40 @@
       }
   } where
       tmap : (i : Obj I) → Hom A (FObj (K I lim) i) (FObj Γ i)
-      tmap i = A [ ( proj i )  o e ]
+      tmap i = A [ proj i o e ]
       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} = {!!}
+      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 
+        ≈↑⟨ car ( pif=q ( prod p (FObj Γ) proj ) {!!} )  ⟩
+              {!!}
+        ≈⟨ {!!} ⟩
+             (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 ⟩
+             proj j o e 
+        ≈↑⟨ idR ⟩
+             (proj j o e ) o id1 A lim
+        ≈⟨⟩
+             tmap j o FMap (K I lim) f
+        ∎ 
+
 
 limit-from :
-      ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
+     ( 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 )
-     ( Γ : 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-ε prod eqa Γ lim p e proj )
+     ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → Equalizer A e f g )
+     ( Γ : 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 {
      limit = λ a t → limit1 a t ;
      t0f=t = λ {a t i } → t0f=t1 {a} {t} {i}  ;
@@ -404,11 +425,11 @@
                 ≈↑⟨ ip-uniqueness (prod p (FObj Γ) proj) ⟩
                       product (prod p (FObj Γ) proj) (λ i → ( proj i o ( e  o f ) ) )
                 ≈⟨ ip-cong  (prod p (FObj Γ) proj) ( λ i → begin
-                    proj i o ( e o f )
+                        proj i o ( e o f )
                 ≈⟨ assoc  ⟩
-                    ( proj i o  e ) o f 
-                ≈⟨  lim=t {i} ⟩
-                    TMap t i
+                        ( proj i o  e ) o f 
+                ≈⟨ lim=t {i} ⟩
+                        TMap t i
                 ∎ ) ⟩
                       product (prod p (FObj Γ) proj) (TMap t)
                 ∎ ) ⟩