# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1379125152 -32400
# Node ID 7e7b2c38dee1ff0311e7bd20cbd2d2931ba7b80f
# Parent  45b81fcb8a644dfb144aa891afcc343c02b32968
every equalizer is monic

diff -r 45b81fcb8a64 -r 7e7b2c38dee1 equalizer.agda
--- a/equalizer.agda	Sat Sep 14 10:04:18 2013 +0900
+++ b/equalizer.agda	Sat Sep 14 11:19:12 2013 +0900
@@ -80,6 +80,34 @@
                   g o ( e  o h )
              ∎
 
+-------------------------------
+-- 
+-- Every equalizer is monic
+--
+--     e i = e j → i = j
+--
+
+monoic : { c a b d : Obj A } {f g : Hom A a b } → {e : Hom A c a } ( eqa : Equalizer A e f g) 
+      →  { i j : Hom A d c }
+      →  A [ A [ equalizer eqa o i ]  ≈  A [ equalizer eqa o j ] ] →  A [ i  ≈ j  ]
+monoic {c} {a} {b} {d} {f} {g} {e} eqa {i} {j} ei=ej = let open ≈-Reasoning (A) in begin
+                 i
+              ≈↑⟨ uniqueness eqa ( begin
+                   equalizer eqa  o i
+              ≈⟨ ei=ej ⟩
+                   equalizer eqa  o j
+              ∎ )⟩
+                 k eqa (equalizer eqa o j) ( f1=gh (fe=ge eqa ) )
+              ≈⟨ uniqueness eqa ( begin
+                   equalizer eqa o ( id c o j )
+              ≈⟨ cdr idL ⟩
+                   equalizer eqa o j
+              ∎ )⟩
+                 id c o j
+              ≈⟨ idL ⟩
+                 j
+              ∎
+
 --------------------------------
 --
 --
@@ -151,6 +179,7 @@
 --     h : c → c'  h' : c' → c
 --     e' = h   o e
 --     e  = h'  o e'
+--         we assume equalizer on fe,ge and fe',ge'
 
 c-iso-l : { 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 )