# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1378583701 -32400
# Node ID 8835015a3e1af1296be1caad9d0b084fc3c999d5
# Parent  c02287d3d2dcb96cb838d93bb3c43b6c38b57f29
passed let;s remove yellow

diff -r c02287d3d2dc -r 8835015a3e1a equalizer.agda
--- a/equalizer.agda	Sun Sep 08 03:56:45 2013 +0900
+++ b/equalizer.agda	Sun Sep 08 04:55:01 2013 +0900
@@ -182,7 +182,7 @@
 c-iso← : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' :  Equalizer A e' f g )
       →  ( keqa :  Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ])  (A [ g o e' ]) )
       →  ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ])   (A [ g o e ]) )
-      →  { e'->e : A [ e'  ≈  A [ e  o equalizer keqa' ] ] }
+      →  { e'->e : A [ e'  ≈  A [ e  o equalizer keqa' ] ] } -- refl
       →  A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ]  ≈ id1 A c ]
 c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' {e'->e} = let open ≈-Reasoning (A) in begin
                  c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa
@@ -282,6 +282,8 @@
      -------                    α(f,g) γ(f,g,α(f,g)j) δ(fα(f,g)j)       =                  α(f,g)j
      -------                           γ(f,g,α(f,g)j) δ(fα(f,g)j)       =                        j
 
+     eefg : {a b c : Obj A} (f g : Hom A a b) {e : Hom A c a} →  Equalizer A e ( A [ f  o  equalizer (eqa f g) ]  ) (A [ g  o  equalizer (eqa f g) ] ) 
+     eefg f g {e} = eqa  ( A [ f  o  equalizer (eqa f g) ]  ) (A [ g  o  equalizer (eqa f g) ] ) 
      lemma-b4 : {d : Obj A} {j : Hom A d c} → A [
           A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o equalizer (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ g o A [ equalizer (eqa f g) o j ] ])) ])
                      (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o
@@ -292,9 +294,23 @@
                      ( k (eqa f g) (( ( equalizer (eqa f g) o j ) o equalizer (eqa (( f o ( equalizer (eqa f g) o j ) )) (( g o ( equalizer (eqa f g) 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 ) ))) )
-             ≈⟨ {!!} ⟩
+             ≈⟨ car ((uniqueness (eqa f g) ( begin
+                         equalizer (eqa f g) o j 
+                ≈↑⟨ idR  ⟩
+                         (equalizer (eqa f g) o j )  o id1 A d
+                ≈⟨⟩
+                        ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g) o j) (g 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) (lemma-equ2 (( 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) o j) (f o equalizer (eqa f g) o j))
+                ≈⟨ {!!} ⟩
+                    id1 A d
+             ∎ ))) ⟩
+                    j o id1 A d
+                ≈⟨ idR ⟩
                     j
-             ∎
+             ∎ 
 
 
 -- end