# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1620468177 -32400
# Node ID 785d8b2ba48f023b5c1459b7695b043b3cb96873
# Parent  cf92383daef578b5fbbccba06d1570ac4ff7cbe4
...

diff -r cf92383daef5 -r 785d8b2ba48f src/ToposIL.agda
--- a/src/ToposIL.agda	Sat May 08 13:02:41 2021 +0900
+++ b/src/ToposIL.agda	Sat May 08 19:02:57 2021 +0900
@@ -116,9 +116,17 @@
         → p ⊢ q → q ⊢ p →  A [ Poly.f p ≈ Poly.f q ]
      tl01 {a} {b} p q p<q q<p = begin
           Poly.f p ≈↑⟨ tt p ⟩
-          char t (equalizer (Ker t (Poly.f p))) (mm p)  ≈⟨   {!!} ⟩
-          char t (equalizer (Ker t (Poly.f q))) (mm q)  ≈⟨   tt q ⟩
+          char t (equalizer (Ker t (Poly.f p))) (mm p)   ≈↑⟨  IsTopos.char-iso (Topos.isTopos t) {!!} {!!}  ⟩
+          char t (equalizer (Ker t (Poly.f p)) ∙ {!!} ) {!!} ≈⟨ {!!} ⟩
+          char t {!!} {!!}   ≈⟨  IsTopos.char-iso (Topos.isTopos t) {!!} {!!}  ⟩
+          char t (equalizer (Ker t (Poly.f p))
+             ∙ IsEqualizer.k (isEqualizer (Ker t (Poly.f p))) (equalizer (Ker t (Poly.f q))) ee1) {!!}   ≈⟨  IsTopos.char-cong (Topos.isTopos t) ee ⟩
+          char t (equalizer (Ker t (Poly.f q))) (mm q)   ≈⟨ tt q  ⟩
           Poly.f q ∎  where
+        ep :  Equalizer A (Poly.f p) (A [ (Topos.⊤ t) o ○ b ])
+        ep = Ker t (Poly.f p)
+        eq :  Equalizer A (Poly.f q) (A [ (Topos.⊤ t) o ○ b ])
+        eq = Ker t (Poly.f q)
         pm : {c : Obj A} (h : Hom A c b ) → A [   Poly.f p ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] → A [   Poly.f q ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] 
         pm h = p<q h
         qm : {c : Obj A} (h : Hom A c b ) → A [   Poly.f q ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] → A [   Poly.f p ∙ h  ≈  (Topos.⊤ t) ∙  ○  c  ] 
@@ -126,8 +134,24 @@
         pp : Hom A b (Topos.Ω t)
         pp =  Poly.f q
         open import equalizer using ( monic )
-        ee : A [ equalizer (Ker t (Poly.f p)) ∙ {!!} ≈ equalizer (Ker t (Poly.f q  ))  ]
-        ee = IsEqualizer.ek=h (Equalizer.isEqualizer (Ker t (Poly.f p))) {{!!}} {{!!}} {{!!}} 
+        fp :  A [ A [ Poly.f p o equalizer (Ker t (Poly.f p)) ]  ≈   A [ A [ (Topos.⊤ t) o  ○  b ] o equalizer (Ker t (Poly.f p)) ]  ]
+        fp = IsEqualizer.fe=ge (Equalizer.isEqualizer (Ker t (Poly.f p))) 
+        fq :  A [ A [ Poly.f q o equalizer (Ker t (Poly.f q)) ]  ≈   A [ A [ (Topos.⊤ t) o  ○  b ] o equalizer (Ker t (Poly.f q)) ]  ]
+        fq = IsEqualizer.fe=ge (Equalizer.isEqualizer (Ker t (Poly.f q))) 
+        ee1 :  A [ A [ Poly.f p o equalizer (Ker t (Poly.f q)) ] ≈ A [ A [ ⊤ t o ○ b ] o equalizer (Ker t (Poly.f q)) ] ]
+        ee1 = begin
+           Poly.f p o equalizer (Ker t (Poly.f q)) ≈⟨ q<p _ ( begin
+            Poly.f q ∙ equalizer (Ker t (Poly.f q)) ≈⟨ fq ⟩
+            ( ⊤ t ∙ ○ b ) ∙ equalizer (Ker t (Poly.f q)) ≈↑⟨ assoc ⟩
+            ⊤ t ∙ ( ○ b  ∙ equalizer (Ker t (Poly.f q))) ≈⟨ cdr e2 ⟩
+            ⊤ t ∙ ○ (equalizer-c (Ker t (Poly.f q)))  ∎ ) ⟩
+           ⊤ t ∙ ○ (equalizer-c (Ker t (Poly.f q))) ≈↑⟨ cdr e2 ⟩
+           ⊤ t ∙ ( ○ b ∙  equalizer (Ker t (Poly.f q) ))  ≈⟨ assoc ⟩
+           (⊤ t ∙ ○ b) ∙  equalizer (Ker t (Poly.f q) )  ∎  where
+        ee : A [ equalizer (Ker t (Poly.f p)) ∙
+           IsEqualizer.k (Equalizer.isEqualizer (Ker t (Poly.f p))) (equalizer (Ker t (Poly.f q  ))) ee1 
+              ≈ equalizer (Ker t (Poly.f q  ))  ]
+        ee = IsEqualizer.ek=h (Equalizer.isEqualizer (Ker t (Poly.f p))) 
         mm : (q : Poly a  (Topos.Ω t) b ) → Mono A  (equalizer (Ker t (Poly.f q)))
         mm q = record { isMono = λ f g →  monic (Ker t (Poly.f q)) }
         tt :  (q : Poly a  (Topos.Ω t) b ) → A [ char t (equalizer (Ker t (Poly.f q))) (mm q) ≈  Poly.f q ]
diff -r cf92383daef5 -r 785d8b2ba48f src/equalizer.agda
--- a/src/equalizer.agda	Sat May 08 13:02:41 2021 +0900
+++ b/src/equalizer.agda	Sat May 08 19:02:57 2021 +0900
@@ -277,6 +277,16 @@
 
 -- c-iso-rl is obvious from the symmetry
 
+equ-iso : { c c' a b : Obj A } {f g : Hom A a b } →  {e : Hom A c a } { e' : Hom A c' a }
+       ( eqa : IsEqualizer A e f g) → ( eqa' :  IsEqualizer A e' f g )
+      → Iso A c c'
+equ-iso eqa eqa' = record {
+      ≅→ = c-iso-l eqa eqa'
+    ; ≅← = c-iso-r eqa eqa'
+    ; iso→ = c-iso-lr eqa' eqa
+    ; iso←  = c-iso-lr eqa eqa'
+   }
+
 --
 -- we cannot have equalizer ≈ id. we only have Iso A (equalizer-c equ) a
 --