# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1620441977 -32400
# Node ID ff1d4188f94da0dba452022eb1daa8a2f1dc59db
# Parent  849f85e543f1a8cb2e164209f04e703628c27939
...

diff -r 849f85e543f1 -r ff1d4188f94d src/CCC.agda
--- a/src/CCC.agda	Sat May 08 10:04:34 2021 +0900
+++ b/src/CCC.agda	Sat May 08 11:46:17 2021 +0900
@@ -232,15 +232,15 @@
      field
          char-uniqueness  : {a b : Obj A } {h : Hom A a Ω}  
              → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
-         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'  ]
-         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 c : Obj A } {m : Hom A a b}  {h : Hom A  b Ω}( mono : Mono A m ) → ( i : Iso A a (equalizer-c (Ker h))  )
+         char-iso  : {a b c : 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-iso  {a} {b} {c} {m} {h} mono i = begin
-            char ( m o Iso.≅← i ) (iso-mono A mono i) ≈⟨ char-cong {!!} ⟩
-            char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h) }) ≈⟨ char-uniqueness {b} {a} {h} ⟩
-            h ∎  where   open ≈-Reasoning A
+         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-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'} {mono} {mono'}  m=m'  = begin
+            char m mono ≈⟨ {!!}   ⟩
+            char (equalizer (Ker {!!})) {!!}  ≈⟨ {!!}   ⟩
+            char m' mono' ∎  where   open ≈-Reasoning A
      ker : {a : Obj A} → ( h : Hom A a Ω )  → Hom A ( equalizer-c (Ker h) ) a
      ker h = equalizer (Ker h)
      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 ] ]