Mercurial > hg > Members > kono > Proof > category

changeset 226:27f2c77c963f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 05 Sep 2013 20:10:51 +0900
parents 1a9f20917fbd
children 591efd381c82
files equalizer.agda
diffstat 1 files changed, 38 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Thu Sep 05 14:56:35 2013 +0900
+++ b/equalizer.agda	Thu Sep 05 20:10:51 2013 +0900
@@ -58,6 +58,9 @@
 f1=g1 : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → (h : Hom A c a) →  A [ A [ f o h ] ≈ A [ g o h ]  ]
 f1=g1 eq h = let open ≈-Reasoning (A) in (resp refl-hom eq )
 
+f1=f1 : { a b : Obj A } (f : Hom A a b ) →  A [ A [ f o (id1 A a)  ] ≈ A [ f o (id1 A a)  ]  ]
+f1=f1  f = let open ≈-Reasoning (A) in refl-hom 
+
 f1=gh : { a b c d : Obj A } {f g : Hom A a b } → { e : Hom A c a } → { h : Hom A d c } →
        (eq : A [ A [ f  o e ] ≈ A [ g  o e ] ] ) → A [ A [ f o A [ e o h ] ] ≈ A [ g o A [ e  o h ]  ] ]
 f1=gh {a} {b} {c} {d} {f} {g} {e} {h} eq = let open ≈-Reasoning (A) in 
@@ -383,23 +386,39 @@
 -- If we have two equalizers on c and c', there are isomorphic pair h, h'
 --
 --     h : c → c'  h' : c' → c
---
+--             h h' = 1 and h' h = 1
 --     not yet done
 
 
-iso-rev  : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {c} f g) →  Hom A a c
-iso-rev {a} {b} {c} {f} {g} eq eqa = k  eqa (id1 A a) (f1=g1 eq (id1 A a))
+c-iso-l : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
+      → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
+      → Hom A c c'  
+c-iso-l  eqa eqa' eff' eff  = let open ≈-Reasoning (A) in k eff' (e eqa) refl-hom
+
+c-iso-r : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
+      → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
+      → Hom A c' c   
+c-iso-r  eqa eqa' eff' eff = let open ≈-Reasoning (A) in k eff (e eqa') refl-hom
 
-equalizer-iso-pair  : { a b c : Obj A } {f g : Hom A a b } → {eq : A [ f ≈ g ] } → ( eqa : Equalizer A {c} f g) → 
-         A [ A [ e eqa o iso-rev eq eqa  ]  ≈ id1 A a ] 
-equalizer-iso-pair  {a} {b} {c} {f} {g} {eq} eqa  = ek=h eqa
+c-iso-1 : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
+      → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
+      →  A [ A [ k eqa' (A [ e eqa' o k eff' (id1 A a ) (f1=f1 f) ] ) (f1=gh ( fe=ge eqa' ) ) o  e eff' ]  ≈ id1 A c' ]
+c-iso-1 = {!!}
+
+c-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
+      → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
+      →  A [ A [ c-iso-l eqa eqa' eff' eff  o c-iso-r eqa eqa' eff' eff ]  ≈ id1 A c' ]
+c-iso {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff = let open ≈-Reasoning (A) in begin
+             c-iso-l eqa eqa' eff' eff  o c-iso-r eqa eqa' eff' eff 
+             ≈⟨⟩
+                k eff' (e eqa) refl-hom  o k eff (e eqa') refl-hom
+             ≈⟨  {!!} ⟩
+                id1 A c'
+             ∎
+
 
 -- Equalizer is unique up to iso
 
-equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' :  Equalizer A {c'} f g ) 
-      → Hom A c c'   --- != id1 A c
-equalizer-iso  {c} eqa eqa' = k eqa' (e eqa) (fe=ge eqa)
-
 --
 --        
 --           e eqa f g        f
@@ -449,9 +468,9 @@
       γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h  o (e ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ;  -- Hom A c d
       δ =  λ {a} f → k (eqa f f) (id1 A a)  (lemma-equ2 f); -- Hom A a c
       b1 = fe=ge (eqa f g) ;
-      b2 = lemma-equ5 ;
-      b3 = lemma-equ3 ;
-      b4 = lemma-equ6 
+      b2 = lemma-b2 ;
+      b3 = lemma-b3 ;
+      b4 = lemma-b4 
  } where
      --
      --           e eqa f g        f
@@ -467,8 +486,8 @@
 
      lemma-equ2 : {a b : Obj A} (f : Hom A a b)  → A [ A [ f o id1 A a ]  ≈ A [ f o id1 A a ] ]
      lemma-equ2 f =   let open ≈-Reasoning (A) in refl-hom
-     lemma-equ3 : A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]
-     lemma-equ3 = let open ≈-Reasoning (A) in
+     lemma-b3 : A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]
+     lemma-b3 = let open ≈-Reasoning (A) in
              begin  
                   e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f)
              ≈⟨ ek=h (eqa f f )  ⟩
@@ -486,21 +505,21 @@
              ≈↑⟨ assoc ⟩
                    g o ( h o e (eqa (f o h) ( g o h )))
              ∎
-     lemma-equ5 :  {d : Obj A} {h : Hom A d a} → A [ 
+     lemma-b2 :  {d : Obj A} {h : Hom A d a} → A [ 
                       A [ e (eqa f g) o k (eqa f g) (A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ]
                     ≈ A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ]
-     lemma-equ5 {d} {h} = let open ≈-Reasoning (A) in
+     lemma-b2 {d} {h} = let open ≈-Reasoning (A) in
              begin
                     e (eqa f g) o k (eqa f g) (h o e (eqa (f o h) (g o h))) (lemma-equ4 {a} {b} {c} f g h) 
              ≈⟨ ek=h (eqa f g)  ⟩
                     h o e (eqa (f o h ) ( g o h ))
              ∎
-     lemma-equ6 : {d : Obj A} {j : Hom A d c} → A [ 
+     lemma-b4 : {d : Obj A} {j : Hom A d c} → A [ 
           A [ k (eqa f g) (A [ A [ e (eqa f g) o j ] o e (eqa (A [ f o A [ e (eqa f g) o j ] ]) (A [ g o A [ e (eqa f g) o j ] ])) ])
                      (lemma-equ4 {a} {b} {c} f g (A [ e (eqa f g) o j ])) o 
               k (eqa (A [ f o A [ e (eqa f g) o j ] ]) (A [ f o A [ e (eqa f g) o j ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ e (eqa f g) o j ] ])) ]
               ≈ j ]
-     lemma-equ6 {d} {j} = let open ≈-Reasoning (A) in 
+     lemma-b4 {d} {j} = let open ≈-Reasoning (A) in 
              begin
                      ( k (eqa f g) (( ( e (eqa f g) o j ) o e (eqa (( f o ( e (eqa f g) o j ) )) (( g o ( e (eqa f g) o j ) ))) ))
                             (lemma-equ4 {a} {b} {c} f g (( e (eqa f g) o j ))) o