# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1378388131 -32400
# Node ID ff596cff8183cffdd647ba97b8faf115a10c6c9d
# Parent  591efd381c822e4a288efc5317527c11d8fe71ff
fix

diff -r 591efd381c82 -r ff596cff8183 equalizer.agda
--- a/equalizer.agda	Thu Sep 05 21:34:33 2013 +0900
+++ b/equalizer.agda	Thu Sep 05 22:35:31 2013 +0900
@@ -394,24 +394,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 )
       → Hom A c c'  
-c-iso-l  eqa eqa' eff' eff  = let open ≈-Reasoning (A) in k eff' (e eqa) refl-hom
+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-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
+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
 
 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'))
-             ≈⟨ {!!} ⟩
-                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 k e k = 1c                   e e = e -> e = 1c?
 --    k e k e = 1c' ?
 
@@ -422,7 +438,13 @@
 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
+                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'
              ∎