Mercurial > hg > Members > kono > Proof > category

changeset 675:1298c3655ba7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 03 Nov 2017 20:45:46 +0900
parents 77690b17c5d9
children faf48511f69d
files pullback.agda
diffstat 1 files changed, 12 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Fri Nov 03 18:59:03 2017 +0900
+++ b/pullback.agda	Fri Nov 03 20:45:46 2017 +0900
@@ -320,31 +320,12 @@
 --                                              Γ f o ε i = ε j 
 --
 
-equ-to : {a b : Obj A} {f g : Hom A a b}
-            → (e0 : Equalizer A (Id {_} {_} {_} {A} a) (Id {_} {_} {_} {A} a))
-            → (e1 : Equalizer A f g )
-            → Hom A ( equalizer-c e1 ) ( equalizer-c e0 )
-equ-to {a} {b} e0 e1 = k (isEqualizer e0) (equalizer e1 ) refl-hom 
-       where open ≈-Reasoning (A) 
-
-equ-to' : {a b : Obj A} {f g : Hom A a b}
-            → (e0 : Equalizer A (Id {_} {_} {_} {A} a) (Id {_} {_} {_} {A} a))
-            → (e1 : Equalizer A f g )
-            → Hom A ( equalizer-c e0 ) ( equalizer-c e1 )
-equ-to' {a} {b} e0 e1 = k (isEqualizer e1) (equalizer e0) {!!}
-       where open ≈-Reasoning (A) 
-
 equc : ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
         ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
             → Obj A
 equc prod eqa = equalizer-c (eqa p0id p0id)
    where
-         p0 = iprod (prod (FObj Γ))
-         p0id = let  open ≈-Reasoning (A) in id1 A p0 
-
-equproj : ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
-   (i : Obj I ) → Hom A (iprod (prod (FObj Γ))) (FObj Γ i)  
-equproj prod i = pi (prod (FObj Γ)) i 
+         p0id = let  open ≈-Reasoning (A) in id1 A (iprod (prod (FObj Γ)))
 
 limit-ε :
      ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
@@ -356,12 +337,18 @@
    } where
        lim : Obj A
        lim = equc prod eqa
+       p0 : Obj A
        p0 = iprod (prod (FObj Γ))
        e : Hom A lim p0
        e = let  open ≈-Reasoning (A) in equalizer ( eqa (id1 A p0 ) ( id1 A p0 ) )
+       proj : (i : Obj I) → Hom A p0 (FObj Γ i)
        proj = pi ( prod  (FObj Γ) )
        tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i)
-       tmap i = A [ equproj prod i o e ] 
+       tmap i = A [ proj i o e ] 
+       e-inv : {i j : Obj I} {f : Hom I i j} → Hom A p0 ( equalizer-c (eqa (A [ FMap Γ f o  proj i ]) ( proj j )) )
+       e-inv = {!!}
+       e-iso : {i j : Obj I} {f : Hom I i j} → A [ A [ equalizer (eqa (A [ FMap Γ f o  proj i ]) ( proj j )) o e-inv ] ≈ id1 A p0 ]
+       e-iso = {!!}
        commute1 :  {i j : Obj I} {f : Hom I i j} →
          A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ]
        commute1 {i} {j} {f} =  let  open ≈-Reasoning (A) in begin
@@ -371,10 +358,10 @@
          ≈⟨ assoc ⟩
               ( FMap Γ f o  proj i ) o e 
          ≈⟨ {!!} ⟩
-              ( ( FMap Γ f o  proj i ) o (equalizer (eqa (FMap Γ f o  proj i) ( proj j )))) o  (( equ-to' (eqa (id1 A p0)(id1 A p0)) (eqa (FMap Γ f o  proj i) ( proj j ))) o k (isEqualizer (eqa (id1 A p0) (id1 A p0) )) (iproduct (isIProduct (prod (FObj Γ))) ({!!})) refl-hom )
-         ≈⟨ car (fe=ge (isEqualizer (eqa (FMap Γ f o  proj i) ( proj j )))) ⟩
-              (  proj j  o (equalizer (eqa (FMap Γ f o  proj i) ( proj j )))) o {!!}
-         ≈⟨ {!!}  ⟩ 
+              ((( FMap Γ f o  proj i ) o equalizer (eqa (FMap Γ f o  proj i) ( proj j ))) o {!!} ) o  e
+         ≈⟨ car ( car (fe=ge (isEqualizer (eqa (FMap Γ f o  proj i) ( proj j ))))) ⟩
+              ((proj j o equalizer (eqa (FMap Γ f o  proj i) ( proj j ))) o {!!} ) o  e
+         ≈⟨ {!!} ⟩
               proj j o e 
          ≈↑⟨ idR ⟩
               (proj j o e ) o id1 A lim