Mercurial > hg > Members > kono > Proof > category

changeset 229:68b2681ea9df

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
c in equalizer is equal up to iso done.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 06 Sep 2013 11:52:41 +0900
parents ff596cff8183
children 1ef8c70c7054
files equalizer.agda
diffstat 1 files changed, 23 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Thu Sep 05 22:35:31 2013 +0900
+++ b/equalizer.agda	Fri Sep 06 11:52:41 2013 +0900
@@ -392,62 +392,40 @@
 
 
 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 )
+      →  ( keqa : Equalizer A {c} (A [ f o e eqa' ])  (A [ g o e eqa' ]) )
       → Hom A c c'  
-c-iso-l  {c} {c'} eqa eqa' eff' eff  = let open ≈-Reasoning (A) in k eff' (A [ e eqa  o id1 A c ]) refl-hom
+c-iso-l  {c} {c'} eqa eqa' keqa = e keqa
 
 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  {c} {c'} eqa eqa' eff' eff = let open ≈-Reasoning (A) in k eff (A [ e eqa'  o id1 A c' ]) refl-hom
+      →  ( keqa : Equalizer A {c} (A [ f o e eqa' ])  (A [ g o e eqa' ]) )
+      →  Hom A c' c   
+c-iso-r  {c} {c'} eqa eqa' keqa = let open ≈-Reasoning (A) in k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )
 
-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 [  e (eefeg eqa') o k (eefeg eqa') (id1 A c')  (f1=g1 (fe=ge eqa') (id1 A c')) ]  ≈ id1 A c' ]
-c-iso-1 {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff =  let open ≈-Reasoning (A) in begin
-                e (eefeg eqa') o k (eefeg eqa') (id1 A c')  (f1=g1 (fe=ge eqa') (id1 A c'))
-             ≈⟨ ek=h ( eefeg eqa' )⟩
-                id1 A c'
-             ∎
 
-c-iso-2 : { 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 [  k eqa' ( A [ e eqa' o id1 A c' ] ) (f1=gh (fe=ge eqa' )) ≈ id1 A c' ]
-c-iso-2 {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff =  let open ≈-Reasoning (A) in begin
-                 k eqa' ( A [ e eqa' o id1 A c' ] ) (f1=gh (fe=ge eqa' ) )
-             ≈⟨ uniqueness eqa' refl-hom ⟩
-                id1 A c'
-             ∎
-
-c-iso-3 : { 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 [  k eff' ( A [ e eff' o id1 A c' ] ) (f1=gh (fe=ge eff')) ≈ id1 A c' ]
-c-iso-3 {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff =  let open ≈-Reasoning (A) in begin
-                 k eff' ( A [ e eff' o id1 A c' ] ) (f1=gh (fe=ge eff'))
-             ≈⟨ uniqueness eff' refl-hom ⟩
-                id1 A c'
-             ∎
+     --             e(eqa')       f
+     --         c'----------> a ------->b               f e j = g e j 
+     --         ^                 g     
+     --         |k      h                   
+     --         |                                        h =   e(eqaj) o k     jhek = jh (uniqueness)
+     --         |         
+     --         c     j o (k (eqa ef ef) j ) = id c      h =   e(eqaj) 
+     --          
+     --                 h j e f = h j e g    →    h =  'j e f 
+     --                                           h =   j e f   -> j = j'
+     --
 
 --    e k e k = 1c                   e e = e -> e = 1c?
 --    k e k e = 1c' ?
 
 
 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  o id1 A c) refl-hom  o k eff (e eqa'  o id1 A c') refl-hom
-             ≈⟨  car ( uniqueness eff' ( begin
-                     e eff' o k eff' {!!} {!!}
-                 ≈⟨ {!!} ⟩
-                     e eqa o id1 A c
-             ∎ ))  ⟩
-                {!!} o k eff (e eqa'  o id1 A c') refl-hom
-             ≈⟨  {!!} ⟩
-                id1 A c'
-             ∎
+      →  ( keqa : Equalizer A {c} (A [ f o e eqa' ])  (A [ g o e eqa' ]) )
+      →  A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ]  ≈ id1 A c' ]
+c-iso {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin
+                 c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa
+              ≈⟨ ek=h keqa ⟩
+                 id1 A c'
+              ∎
 
 
 -- Equalizer is unique up to iso