--- a/equalizer.agda	Thu Sep 05 20:10:51 2013 +0900
+++ b/equalizer.agda	Thu Sep 05 21:34:33 2013 +0900
@@ -49,6 +49,7 @@
    β {d} {e} {a} {b} f g h =  A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ] 
 
 open Equalizer
+
 open Burroni
 
 --
@@ -326,9 +327,9 @@
       
 --  If we have equalizer f g, e (ef) (eg) is also an equalizer  and e = id c
 
-eefeg : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) 
+eefeg : {a b c : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) 
            → Equalizer A {c} (A [ f o e eqa ])  (A [ g o e eqa ] ) 
-eefeg {a} {b} {c} {d} {f} {g} eqa =  record {
+eefeg {a} {b} {c} {f} {g} eqa =  record {
       e = id1 A c ; -- i  ; -- A [ h-1 o e eqa ]  ;       -- Hom A a d
       fe=ge = fe=ge1 ;
       k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ;
@@ -402,8 +403,18 @@
 
 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 = {!!}
+      →  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'
+             ∎
+
+--    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 )