--- a/equalizer.agda	Sun Sep 08 06:43:20 2013 +0900
+++ b/equalizer.agda	Sun Sep 08 11:54:06 2013 +0900
@@ -38,9 +38,12 @@
       α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) →  {e : Hom A c a } → Hom A c a
       γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →  Hom A d c
       δ : {a b c : Obj A } → {e : Hom A c a } → (f : Hom A a b) → Hom A a c
+      cong-α : {a b c :  Obj A } → {g g' : Hom A a b } →  A [ g ≈ g' ] → { α α' : Hom A c a } → A [ α ≈ α' ] 
+      cong-γ : {a _ c d : Obj A } → {h h' : Hom A d a } →  A [ h ≈ h' ] →  { γ γ' : Hom A d c } → A [ γ ≈ γ' ] 
+      cong-δ : {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → { δ δ' : Hom A a c } → A [ δ ≈ δ' ] 
       b1 : A [ A [ f  o α {a} {b} {c}  f g {e} ] ≈ A [ g  o α {a} {b} {c} f g {e} ] ]
       b2 :  {d : Obj A } → {h : Hom A d a } → A [ A [ ( α {a} {b} {c} f g {e} ) o (γ {a} {b} {c} f g h) ] ≈ A [ h  o α (A [ f o h ]) (A [ g o h ]){id1 A d} ] ]
-      b3 :  A [ A [ α {a} {b} {a} f f {id1 A a} o δ {a} {b} {a} {id1 A a} f ] ≈ id1 A a ]
+      b3 : {a b d : Obj A} → (f : Hom A a b ) → {h : Hom A d a } → A [ A [ α {a} {b} {d} f f {h} o δ {a} {b} {d} {h} f ] ≈ id1 A a ]
       -- b4 :  {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o  k ] ) ≈ k ]
       b4 :  {d : Obj A } {k : Hom A d c} → 
            A [ A [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g {e} o k ] ) o ( δ {d} {b} {d} {id1 A d} (A [ f o A [ α {a} {b} {c} f g {e} o  k ] ] )  )] ≈ k ]
@@ -227,11 +230,20 @@
       α = λ {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
+      cong-α = cong-α1 ;
+      cong-γ = cong-γ1 ;
+      cong-δ = cong-δ1  ;
       b1 = fe=ge (eqa {a} {b} {c} f g {e}) ;
       b2 = lemma-b2 ;
       b3 = lemma-b3 ;
       b4 = lemma-b4
  } where
+     cong-α1 : {a b c :  Obj A } → {g g' : Hom A a b } →  A [ g ≈ g' ] → { α α' : Hom A c a } → A [ α ≈ α' ]
+     cong-α1 {a} {b} {c} {g} {g'} eq  = let open ≈-Reasoning (A) in  {!!}
+     cong-γ1 :  {a _ c d : Obj A } → {h h' : Hom A d a } →  A [ h ≈ h' ] →  { γ γ' : Hom A d c } → A [ γ ≈ γ' ]
+     cong-γ1 = {!!} 
+     cong-δ1 :  {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → { δ δ' : Hom A a c } → A [ δ ≈ δ' ]
+     cong-δ1 =  {!!} 
      --
      --           e eqa f g        f
      --         c ----------> a ------->b
@@ -246,8 +258,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-b3 : A [ A [ equalizer (eqa f f ) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]
-     lemma-b3 = let open ≈-Reasoning (A) in
+     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} f {h} = let open ≈-Reasoning (A) in
              begin
                   equalizer (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f)
              ≈⟨ ek=h (eqa f f )  ⟩
@@ -331,19 +343,25 @@
                   ( h o ( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) 
              ≈↑⟨ assoc ⟩
                    h o ((( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h)  )
-             ≈⟨ cdr {!!} ⟩
+             ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩
+                   h o ((( α bur ( f o h ) ( f o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h)  )
+             ≈⟨ cdr (b3 bur {d} {b} {d} (f  o h) {id1 A d} ) ⟩
                    h o id1 A d
-             ≈⟨ {!!}  ⟩
+             ≈⟨ idR ⟩
                  h 
              ∎
       uniqueness1 : {d : Obj A} →  ∀ {h : Hom A d a} →  {eq : A [ A [ f  o  h ] ≈ A [ g  o h ] ] } →  {k' : Hom A d c } →
               A [ A [ (α bur f g)  o k' ] ≈ h ] → A [ k1 {d} h eq  ≈ k' ]
       uniqueness1 {d} {h} {eq} {k'} ek=h =   let open ≈-Reasoning (A) in
              begin
-                 k1 {d} h eq
+                k1 {d} h eq
              ≈⟨⟩
-                 γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} {id1 A d} (f o h)
-             ≈⟨ ? ⟩
+                γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} {id1 A d} (f o h)
+             ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩
+                γ bur f g (A [ α bur f g o k' ]) o δ bur {d} {b} {d} {id1 A d} (f o h)
+             ≈↑⟨ cdr (cong-δ bur {d} {a} {d} (resp {d} {d} {a} {id1 A d} refl-hom ek=h )) ⟩
+                γ bur f g (A [ α bur f g o k' ]) o δ bur (A [ f o A [ α bur f g o k' ] ])
+             ≈⟨ b4 bur ⟩
                  k'
              ∎