--- a/src/CCC.agda	Sun May 09 00:20:48 2021 +0900
+++ b/src/CCC.agda	Sun May 09 16:52:27 2021 +0900
@@ -190,6 +190,9 @@
 
 open Mono
 
+eMonic : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} { f g : Hom A b a } → (equ : Equalizer A f g ) → Mono A (equalizer equ)
+eMonic A equ = record { isMono = λ f g → monic equ }
+
 iso-mono :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {m : Hom A a b}  ( mono : Mono A m ) (i : Iso A a c ) → Mono A (A [ m o Iso.≅← i ] )
 iso-mono A {a} {b} {c} {m} mono i = record { isMono = λ {d} f g → im  f g } where
      im : {d : Obj A} (f g : Hom A d c ) →   A [ A [ A [ m o Iso.≅← i ]  o f ] ≈ A [  A [ m o Iso.≅← i ] o g ] ] → A [ f ≈ g ]
@@ -246,27 +249,15 @@
         (char : {a b : Obj A} → (m :  Hom A b a) → Mono A m  → Hom A a Ω) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
          ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ])
-         char-iso  : {a b : Obj A } {m : Hom A a b}  {h : Hom A  b Ω}( mono : Mono A m ) → ( i : Iso A a (equalizer-c (Ker h))  )
-             → A [ char (A [ m o Iso.≅← i ]) (iso-mono A mono i) ≈ h ]
-         char-cong  : {a b : Obj A } { m m' :  Hom A b a } { mono : Mono A m } { mono' : Mono A m' }
+         char-uniqueness  : {a b : Obj A } {h : Hom A a Ω}  
+             → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
+         char-iso :  {a a' b : Obj A} → (p : Hom A a b ) (q : Hom A a' b ) → (mp : Mono A p) →(mq : Mono A q) →
+                Iso A a a'  → A [ char p mp  ≈ char q mq ]
+     char-cong  : {a b : Obj A } { m m' :  Hom A b a } { mono : Mono A m } { mono' : Mono A m' }
              → A [ m  ≈  m'  ] → A [ char m mono ≈ char m' mono'  ]
+     char-cong {a} {b} {m} {m'} {mo} {mo'} m=m' = char-iso m m' mo mo' (≡-iso A _)
      ker : {a : Obj A} → ( h : Hom A a Ω )  → Hom A ( equalizer-c (Ker h) ) a
      ker h = equalizer (Ker h)
-     char-uniqueness  : {a b : Obj A } {h : Hom A a Ω}  
-             → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
-     char-uniqueness {a} {b} {h}  = begin
-            char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈⟨ char-cong (
-              begin
-              equalizer (Ker h)  ≈↑⟨ idR ⟩
-              equalizer (Ker h) o id1 A _  ≈↑⟨ cdr (idR) ⟩
-              equalizer (Ker h) o ( id1 A _   o id1 A _ )  ≈⟨ assoc ⟩
-              (equalizer (Ker h)  o  Iso.≅→ (≡-iso A _))  o Iso.≅← (≡-iso A _) ∎ ) ⟩
-            char ( ( equalizer (Ker h)  o  Iso.≅→ (≡-iso A _))  o Iso.≅← (≡-iso A _) ) (iso-mono A (≡-mono→ h) (≡-iso A _)) ≈⟨ char-iso (≡-mono→ h) (≡-iso A _) ⟩
-            h ∎  where
-        open ≈-Reasoning A
-        ≡-mono→ : {a : Obj A } (h : Hom A a Ω) →
-            Mono A ( equalizer (Ker h) o (Iso.≅→ (≡-iso A (equalizer-c (Ker h)))))
-        ≡-mono→ {a} h = iso-mono→ A (record { isMono =  λ f g → monic (Ker h)}  ) (≡-iso A _)
      char-m=⊤ :  {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m) → A [ A [ char m mono  o m ] ≈ A [ ⊤ o CCC.○ c b ] ]
      char-m=⊤ {a} {b} m mono  = begin
             char m mono  o m ≈⟨ IsEqualizer.fe=ge (ker-m m mono)  ⟩