Mercurial > hg > Members > kono > Proof > category

changeset 249:bdeed843f8b1

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 Mon, 09 Sep 2013 14:03:44 +0900
parents efa2fd0e91ee
children a1e2228c2a6b
files equalizer.agda
diffstat 1 files changed, 12 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Mon Sep 09 12:55:36 2013 +0900
+++ b/equalizer.agda	Mon Sep 09 14:03:44 2013 +0900
@@ -81,7 +81,7 @@
 
 --
 --
---   An isomorphic element c' of c makes another equalizer
+--   An isomorphic arrow c' to c makes another equalizer
 --
 --           e eqa f g        f
 --         c ----------> a ------->b
@@ -224,7 +224,6 @@
 --
 -- An equalizer satisfies Burroni equations
 --
---    congs are not yet done
 ----
 
 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b)  → (e : Hom A c a ) →
@@ -234,7 +233,7 @@
       α = λ {a} {b} {c}  f g e  →  equalizer (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a
       γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h  o (equalizer ( eqa (A [ f  o  h ] ) (A [ g o h ] ))) ] ) 
                             (lemma-equ4 {a} {b} {c} {d} f g h ) ;  -- Hom A c d
-      δ =  λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (lemma-equ2 f); -- Hom A a c
+      δ =  λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (f1=f1 f); -- Hom A a c
       cong-α = λ {a b c e f g g'} eq → cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq ;
       cong-γ = λ {a} {_} {c} {d} {f} {g} {h} {h'} eq → cong-γ1 {a}  {c} {d} {f} {g} {h} {h'} eq  ;
       cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {e} {f} {f'} f=f'  ;
@@ -255,12 +254,10 @@
      --
      --               e  o id1 ≈  e  →   k e  ≈ id
 
-     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-b3 : {a b d : Obj A} (f : Hom A a b ) { h : Hom A d a } → A [ A [ equalizer (eqa f f ) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a  ]
+     lemma-b3 : {a b d : Obj A} (f : Hom A a b ) { h : Hom A d a } → A [ A [ equalizer (eqa f f ) o k (eqa f f) (id1 A a) (f1=f1 f) ] ≈ id1 A a  ]
      lemma-b3 {a} {b} {d} f {h} = let open ≈-Reasoning (A) in
              begin
-                  equalizer (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f)
+                  equalizer (eqa f f) o k (eqa f f) (id1 A a) (f1=f1 f)
              ≈⟨ ek=h (eqa f f )  ⟩
                   id1 A a
              ∎
@@ -293,17 +290,17 @@
              ∎ )⟩    
                  k (eqa f g ) {d} ( A [ h' o (equalizer ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
              ∎
-     cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] →  A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (lemma-equ2 f)  ≈ 
-                                                                            k (eqa {a} {b} {c} f' f' {e} ) (id1 A a)  (lemma-equ2 f') ]
+     cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] →  A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (f1=f1 f)  ≈ 
+                                                                            k (eqa {a} {b} {c} f' f' {e} ) (id1 A a)  (f1=f1 f') ]
      cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' =  let open ≈-Reasoning (A) in
              begin
-                 k (eqa {a} {b} {c} f  f  {e} ) (id1 A a)  (lemma-equ2 f) 
+                 k (eqa {a} {b} {c} f  f  {e} ) (id1 A a)  (f1=f1 f) 
              ≈⟨  uniqueness (eqa f f) ( begin
-                 e o k (eqa {a} {b} {c} f' f' {e} ) (id1 A a)  (lemma-equ2 f') 
+                 e o k (eqa {a} {b} {c} f' f' {e} ) (id1 A a)  (f1=f1 f') 
              ≈⟨ ek=h (eqa {a} {b} {c} f' f' {e} ) ⟩
                  id1 A a
              ∎ )⟩
-                 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a)  (lemma-equ2 f') 
+                 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a)  (f1=f1 f') 
              ∎
 
      lemma-b2 :  {d : Obj A} {h : Hom A d a} → A [
@@ -320,13 +317,13 @@
               A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o 
                  equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ])
                      (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o
-              k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ equalizer (eqa f g) o j ] ])) ]
+              k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ])) (id1 A d) (f1=f1 (A [ f o A [ equalizer (eqa f g) o j ] ])) ]
               ≈ j ]
      lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
              begin
                 ( k (eqa f g) (( ( equalizer (eqa f g) o j ) o equalizer (eqa (( f o ( equalizer (eqa f g {e}) o j ) )) (( g o ( equalizer (eqa f g {e}) o j ) ))) ))
                             (lemma-equ4 {a} {b} {c} f g (( equalizer (eqa f g) o j ))) o
-                   k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) )
+                   k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer (eqa f g) o j ) ))) )
              ≈⟨ car ((uniqueness (eqa f g) ( begin
                          equalizer (eqa f g) o j 
                 ≈↑⟨ idR  ⟩
@@ -334,7 +331,7 @@
                 ≈⟨⟩         -- here we decide e (fej) (gej)' is id1 A d
                         ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g {e}) o j) (g o equalizer (eqa f g {e}) o j)))
              ∎ ))) ⟩
-                    j o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) 
+                    j o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer (eqa f g) o j ) ))) 
              ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) ( begin
                      equalizer (eqa (f o equalizer (eqa f g {e} ) o j) (f o equalizer (eqa f g {e}) o j))  o id1 A d
                 ≈⟨ idR ⟩