# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1613879825 -32400
# Node ID e29b6488b17989f0009ee580c99e8291fa859f8f
# Parent  468288f3dfe504e9abf13d88e2b873c5eaf928ce
b4

diff -r 468288f3dfe5 -r e29b6488b179 src/equalizer.agda
--- a/src/equalizer.agda	Sun Feb 21 10:26:00 2021 +0900
+++ b/src/equalizer.agda	Sun Feb 21 12:57:05 2021 +0900
@@ -297,21 +297,35 @@
                      (lemma-equ4 {a} {b} {d} f g (A [ equalizer (eqa f g) o j ])) 
                  o    k (ieqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ g o A [ equalizer (eqa f g) o j ] ])) (id1 A _)
                      (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))] ≈ j ]
-     lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
+     --   h = equalizer (eqa f g) o j 
+     lemma-b4 {d} {j} = 
              begin
-                 k (ieqa 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} {d} f g (( equalizer (eqa f g) o j )))
-                 o    k (ieqa (f o ( equalizer (eqa f g) o j )) ( g o (equalizer (eqa f g) o j ))) (id1 A _)
-                     (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))
-             ≈⟨ car (uniqueness (ieqa f g) {!!}) ⟩
-                 {!!} o {!!}
-             ≈⟨ cdr (uniqueness (ieqa (f o ( equalizer (eqa f g) o j )) ( g o (equalizer (eqa f g) o j ))) {!!}) ⟩
-                 {!!} o {!!}
-             ≈⟨ {!!} ⟩
+                 k (ieqa f g) (( h o equalizer (eqa (( f o h )) (( g o h ))) )) (lemma-equ4 {a} {b} {d} f g (h))
+                 o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))
+             ≈↑⟨ uniqueness (ieqa f g) ( begin
+                  equalizer (eqa f g) o ( k (ieqa f g) (( h o equalizer (eqa ( f o h ) ( g o h )) )) (lemma-equ4 {a} {b} {d} f g h)
+                   o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _)) )
+                ≈⟨ assoc ⟩
+                 (equalizer (eqa f g) o ( k (ieqa f g) (( h o equalizer (eqa ( f o h ) ( g o h )) )) (lemma-equ4 {a} {b} {d} f g h)))
+                   o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))
+                ≈⟨ car (ek=h (ieqa f g) ) ⟩
+                 (( h o equalizer (eqa ( f o h ) ( g o h )) ))
+                   o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _))
+                ≈↑⟨ assoc ⟩
+                 h o (equalizer (eqa ( f o h ) ( g o h )) o    k (ieqa (f o h) ( g o h)) (id1 A _) (f1=g1 (f1=gh (fe=ge (ieqa f g))) (id1 A _)))
+                ≈⟨ cdr (ek=h  (ieqa (f o h) ( g o h))) ⟩
+                 h o id1 A _
+                ≈⟨ idR ⟩
+                 h
+                ∎ 
+             ) ⟩
+                 k (ieqa f g) h (f1=gh (fe=ge (ieqa f g)) )
+             ≈⟨ uniqueness (ieqa f g) refl-hom ⟩
                  j
-             ∎ 
-
-
+             ∎  where
+               open ≈-Reasoning A
+               h : Hom A d a
+               h = equalizer (eqa f g) o j
 
 
 --------------------------------