Mercurial > hg > Members > kono > Proof > category

changeset 674:77690b17c5d9

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 18:59:03 +0900
parents 0007f9a25e9c
children 1298c3655ba7
files pullback.agda
diffstat 1 files changed, 20 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Fri Nov 03 13:31:08 2017 +0900
+++ b/pullback.agda	Fri Nov 03 18:59:03 2017 +0900
@@ -320,6 +320,20 @@
 --                                              Γ 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
@@ -340,8 +354,10 @@
        TMap = λ i → tmap i ; 
        isNTrans = record { commute = commute1 }
    } where
+       lim : Obj A
        lim = equc prod eqa
        p0 = iprod (prod (FObj Γ))
+       e : Hom A lim p0
        e = let  open ≈-Reasoning (A) in equalizer ( eqa (id1 A p0 ) ( id1 A p0 ) )
        proj = pi ( prod  (FObj Γ) )
        tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i)
@@ -354,8 +370,11 @@
               FMap Γ f o ( proj i o e )
          ≈⟨ assoc ⟩
               ( FMap Γ f o  proj i ) o e 
-         -- ≈⟨ fe=ge (isEqualizer (eqa (FMap Γ f o  proj i) ( proj j ))) ⟩
          ≈⟨ {!!} ⟩
+              ( ( 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 {!!}
+         ≈⟨ {!!}  ⟩ 
               proj j o e 
          ≈↑⟨ idR ⟩
               (proj j o e ) o id1 A lim