# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1379125302 -32400
# Node ID 99751fb809e01a2c48b052d2550092fa5d5239b8
# Parent  80dfdeb3e4e7661e36ab50f554fd3f636093feae
fix

diff -r 80dfdeb3e4e7 -r 99751fb809e0 equalizer.agda
--- a/equalizer.agda	Sat Sep 14 11:20:18 2013 +0900
+++ b/equalizer.agda	Sat Sep 14 11:21:42 2013 +0900
@@ -98,7 +98,11 @@
                    equalizer eqa  o j
               ∎ )⟩
                  k eqa (equalizer eqa o j) ( f1=gh (fe=ge eqa ) )
-              ≈⟨ uniqueness eqa refl-hom ⟩
+              ≈⟨ uniqueness eqa ( begin
+                   equalizer eqa o j
+              ≈⟨⟩
+                   equalizer eqa o j
+              ∎ )⟩
                  j
               ∎