# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1620631443 -32400
# Node ID 918319d070b096538446bdb970c3512741ee7ba4
# Parent  5e89bbb4cf53028c482a87d901098e36fb1f98f1
..

diff -r 5e89bbb4cf53 -r 918319d070b0 src/ToposIL.agda
--- a/src/ToposIL.agda	Sun May 09 17:09:21 2021 +0900
+++ b/src/ToposIL.agda	Mon May 10 16:24:03 2021 +0900
@@ -116,65 +116,37 @@
         → 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 kp ) (eMonic A kp) ≈⟨ IsTopos.char-iso (Topos.isTopos t) (equalizer kp ) (equalizer kq ) (eMonic A kp) (eMonic A kq) pqiso ⟩
-          char t (equalizer kq ) (eMonic A kq) ≈⟨ tt q ⟩
+          char t (equalizer (kp p) ) (eMonic A (kp p)) ≈⟨ IsTopos.char-iso (Topos.isTopos t) (equalizer (kp p) ) (equalizer (kp q) ) (eMonic A (kp p)) (eMonic A (kp q)) pqiso ⟩
+          char t (equalizer (kp q) ) (eMonic A (kp q)) ≈⟨ tt q ⟩
           Poly.f q ∎   where
         open import equalizer using ( monic )
         open IsEqualizer renaming ( k to ek )
-        kp = Ker t ( Poly.f p )
-        kq = Ker t ( Poly.f q )
-        fp :  A [ A [ Poly.f p o equalizer kp ]  ≈   A [ A [ (Topos.⊤ t) o  ○  b ] o equalizer kp ]  ]
-        fp = fe=ge (isEqualizer kp) 
-        fq :  A [ A [ Poly.f q o equalizer kq ]  ≈   A [ A [ (Topos.⊤ t) o  ○  b ] o equalizer kq ]  ]
-        fq = fe=ge (isEqualizer kq) 
-        eeq :  A [ A [ Poly.f p o equalizer kq ] ≈ A [ A [ ⊤ t o ○ b ] o equalizer kq ] ]
-        eeq = begin
-           Poly.f p o equalizer kq ≈⟨ q<p _ ( begin
-            Poly.f q ∙ equalizer kq ≈⟨ fq ⟩
-            ( ⊤ t ∙ ○ b ) ∙ equalizer kq ≈↑⟨ assoc ⟩
-            ⊤ t ∙ ( ○ b  ∙ equalizer kq) ≈⟨ cdr e2 ⟩
-            ⊤ t ∙ ○ (equalizer-c kq)  ∎ ) ⟩
-           ⊤ t ∙ ○ (equalizer-c kq) ≈↑⟨ cdr e2 ⟩
+        kp : (p : Poly a  (Topos.Ω t) b ) →  Equalizer A _ _
+        kp p = Ker t ( Poly.f p )
+        ee :  (p q : Poly a  (Topos.Ω t) b ) →  q ⊢ p
+            →  A [ A [ Poly.f p o equalizer (Ker t ( Poly.f q )) ] ≈ A [ A [ ⊤ t o ○ b ] o equalizer (Ker t ( Poly.f q ))] ]
+        ee p q q<p = begin
+           Poly.f p o equalizer (Ker t ( Poly.f q )) ≈⟨ q<p _ ( begin
+            Poly.f q ∙ equalizer (Ker t ( Poly.f q )) ≈⟨ fe=ge (isEqualizer (Ker t ( Poly.f q))) ⟩
+            ( ⊤ 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
-        qtop : Hom A (equalizer-c kq) (equalizer-c kp)
-        qtop = ek (isEqualizer kp) (equalizer kq) eeq 
-        epq : A [ equalizer kp ∙
-           ek (isEqualizer kp) (equalizer (Ker t (Poly.f q  ))) eeq 
-              ≈ equalizer (Ker t (Poly.f q  ))  ]
-        epq = ek=h (isEqualizer kp) 
-        eep :  A [ A [ Poly.f q o equalizer kp ] ≈ A [ A [ ⊤ t o ○ b ] o equalizer kp ] ]
-        eep = begin
-           Poly.f q o equalizer kp ≈⟨ p<q _ ( begin
-            Poly.f p ∙ equalizer kp ≈⟨ fp ⟩
-            ( ⊤ t ∙ ○ b ) ∙ equalizer kp ≈↑⟨ assoc ⟩
-            ⊤ t ∙ ( ○ b  ∙ equalizer kp) ≈⟨ cdr e2 ⟩
-            ⊤ t ∙ ○ (equalizer-c kp)  ∎ ) ⟩
-           ⊤ t ∙ ○ (equalizer-c kp) ≈↑⟨ cdr e2 ⟩
-           ⊤ t ∙ ( ○ b ∙  equalizer kp )  ≈⟨ assoc ⟩
-           (⊤ t ∙ ○ b) ∙  equalizer kp   ∎  where
-        ptoq : Hom A (equalizer-c kp) (equalizer-c kq)
-        ptoq = ek (isEqualizer kq) (equalizer kp) eep 
-        qq=1 : A [ A [ qtop o ptoq ] ≈ id1 A (equalizer-c kp) ]
-        qq=1 = begin
-           qtop o ptoq ≈↑⟨ uniqueness (isEqualizer kp) (begin
-             equalizer kp ∙ (qtop ∙ ptoq ) ≈⟨ assoc ⟩
-             (equalizer kp ∙ qtop ) ∙ ptoq  ≈⟨ car (ek=h (isEqualizer kp)) ⟩
-             equalizer kq ∙ ptoq   ≈⟨ ek=h (isEqualizer kq) ⟩
-             equalizer kp ∎ ) ⟩
-           ek (isEqualizer kp) (equalizer kp) (fe=ge (isEqualizer kp)) ≈⟨ uniqueness (isEqualizer kp) idR ⟩
-           id1 A _ ∎  where
-        pp=1 : A [ A [ ptoq o qtop ] ≈ id1 A (equalizer-c kq) ]
-        pp=1 = begin
-           ptoq o qtop ≈↑⟨ uniqueness (isEqualizer kq) (begin
-             equalizer kq ∙ (ptoq ∙ qtop ) ≈⟨ assoc ⟩
-             (equalizer kq ∙ ptoq ) ∙ qtop  ≈⟨ car (ek=h (isEqualizer kq)) ⟩
-             equalizer kp ∙ qtop   ≈⟨ ek=h (isEqualizer kp) ⟩
-             equalizer kq ∎ ) ⟩
-           ek (isEqualizer kq) (equalizer kq) (fe=ge (isEqualizer kq)) ≈⟨ uniqueness (isEqualizer kq) idR ⟩
-           id1 A _ ∎  where
-        pqiso : Iso A (equalizer-c kp) (equalizer-c kq)
-        pqiso = record { ≅→ = ptoq ; ≅← = qtop ; iso→  = qq=1 ; iso← = pp=1 } 
+           (⊤ t ∙ ○ b) ∙  equalizer (Ker t (Poly.f q) )  ∎  
+        qtop : (p q : Poly a  (Topos.Ω t) b ) →  q ⊢ p →  Hom A (equalizer-c (Ker t ( Poly.f q ))) (equalizer-c (Ker t ( Poly.f p )))
+        qtop p q q<p = ek (isEqualizer (Ker t ( Poly.f p))) (equalizer (Ker t ( Poly.f q))) (ee p q q<p)
+        qq=1 : (p q : Poly a  (Topos.Ω t) b ) →  (q<p : q ⊢ p ) → (p<q : p ⊢ q) → A [ A [ qtop p q q<p o qtop q p p<q ] ≈ id1 A (equalizer-c (Ker t ( Poly.f p ))) ]
+        qq=1 p q q<p p<q = begin
+           qtop  p q q<p o qtop q p p<q  ≈↑⟨ uniqueness (isEqualizer (Ker t ( Poly.f p ))) (begin
+             equalizer (kp p) ∙ (qtop  p q q<p ∙ qtop q p p<q  ) ≈⟨ assoc ⟩
+             (equalizer (kp p) ∙ qtop  p q q<p ) ∙ qtop q p p<q   ≈⟨ car (ek=h (isEqualizer (kp p))) ⟩
+             equalizer (kp q) ∙ qtop q p p<q    ≈⟨ ek=h (isEqualizer (kp q)) ⟩
+             equalizer (kp p) ∎ ) ⟩
+           ek (isEqualizer (kp p)) (equalizer (kp p)) (fe=ge (isEqualizer (kp p))) ≈⟨ uniqueness (isEqualizer (kp p)) idR ⟩
+           id1 A _ ∎  
+        pqiso : Iso A (equalizer-c (kp p)) (equalizer-c (kp q))
+        pqiso = record { ≅← = qtop  p q q<p ; ≅→ =  qtop q p p<q ; iso→  = qq=1 p q q<p p<q  ; iso← = qq=1 q p p<q q<p  } 
         tt :  (q : Poly a  (Topos.Ω t) b ) → A [ char t (equalizer (Ker t (Poly.f q))) (eMonic A (Ker t (Poly.f q)))  ≈  Poly.f q ]
         tt q = IsTopos.char-uniqueness (Topos.isTopos t) {b} {a} 
 
@@ -185,9 +157,6 @@
 
      ---  Poly.f p ∙  h  ≈  ⊤ ∙  ○  c 
      ---  Poly.f q ∙  h  ≈  ⊤ ∙  ○  c 
-     il01 : {a b : Obj A}  (p : Poly a  Ω b ) (q : Poly a  Ω b )
-        → p ⊢ q → q ⊢ p →  A [ Poly.f p ≈ Poly.f q ]
-     il01 {a} p q p<q q<p = {!!} 
 
      il011 : {a b : Obj A}  (p q q1 : Poly a  Ω b ) 
         → q ⊢ p → q , q1 ⊢ p