# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1620546747 -32400
# Node ID 10b4d04b734f1063ca2717c2b152594ca25ac911
# Parent  2755bac8d8b92691b81c4104778c13f36c6605cb
fix topos char iso

diff -r 2755bac8d8b9 -r 10b4d04b734f src/CCC.agda
--- 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)  ⟩
diff -r 2755bac8d8b9 -r 10b4d04b734f src/CCCSets.agda
--- a/src/CCCSets.agda	Sun May 09 00:20:48 2021 +0900
+++ b/src/CCCSets.agda	Sun May 09 16:52:27 2021 +0900
@@ -137,7 +137,8 @@
       ;  char = λ m mono → tchar m mono
       ;  isTopos = record {
                  char-uniqueness  = λ {a} {b} {h} →  extensionality Sets ( λ x → uniq h x )
-              ;  ker-m = λ m mono → equalizerIso _ _ (tker (tchar m mono)) m (isol m mono) 
+              ;  char-iso  = iso-m
+              ;  ker-m = ker-iso 
          }
     } where
 --
@@ -200,10 +201,11 @@
         s2i  : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (e : sequ a Bool (tchar m mono)  (λ _ → true )) → image m (equ e)
         s2i {a} {b} m mono (elem y eq) with lem (image m y)
         ... | case1 im = im
-        isol : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → IsoL Sets m (λ (e : sequ a Bool (tchar m mono)  (λ _ → true )) → equ e )
-        isol {a} {b} m mono  = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ;
-               iso→  =  extensionality Sets ( λ x → iso1 x )
-             ; iso←  =  extensionality Sets ( λ x → iso2 x) } ; iso≈L = extensionality Sets ( λ s → iso3 s ) } where
+        iso-m :  {a a' b : Obj Sets} (p : Hom Sets a b) (q : Hom Sets a' b) (mp : Mono Sets p) (mq : Mono Sets q) →
+            Iso Sets a a' → Sets [ tchar p mp ≈ tchar q mq ]
+        iso-m {a} {a'} {b} p q mp mq i = {!!}
+        ker-iso :  {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true) o CCC.○ sets a ])
+        ker-iso {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m  isol (extensionality Sets ( λ x → iso4 x)) where
           b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true))
           b→s x = b2s m mono x
           b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b
@@ -219,6 +221,11 @@
              i2b m (isImage x)  ≡⟨⟩
              x ∎ where open ≡-Reasoning
           iso1 x | false | record { eq = eq1 } = ⊥-elim ( tchar¬Img m mono (m x) eq1 (isImage x))
+          iso4 : (x : b ) →  (Sets [ Equalizer.equalizer (tker (tchar m mono)) o b→s ]) x ≡ m x
+          iso4 x = begin 
+             equ (b2s m mono x) ≡⟨ sym (iso3 (b2s m mono x)) ⟩
+             m (b←s (b2s m mono x)) ≡⟨ cong (λ k → m k ) (iso1 x) ⟩
+             m x ∎ where open ≡-Reasoning
           iso2 : (x : sequ a Bool (tchar m mono) (λ _ → true) ) →  (Sets [ b→s o b←s ]) x ≡ id1 Sets (sequ a Bool (tchar m mono) (λ _ → true)) x
           iso2 (elem y eq) = begin
              b→s ( b←s (elem y eq)) ≡⟨⟩
@@ -240,7 +247,10 @@
                ... | true | record {eq = eq1} = refl
                ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1
                ... | t = ⊥-elim (t (isImage x)) 
-
+          isol :  Iso Sets b (Equalizer.equalizer-c (tker (tchar m mono)))
+          isol = record { ≅→ = b→s ; ≅← = b←s ;
+                iso→  =  extensionality Sets ( λ x → iso1 x )
+              ; iso←  =  extensionality Sets ( λ x → iso2 x) } -- ; iso≈L = extensionality Sets ( λ s → iso3 s ) } where
           open import Polynominal (Sets {c} )  (sets {c})
           A = Sets {c}
           Ω = Bool
diff -r 2755bac8d8b9 -r 10b4d04b734f src/ToposIL.agda
--- a/src/ToposIL.agda	Sun May 09 00:20:48 2021 +0900
+++ b/src/ToposIL.agda	Sun May 09 16:52:27 2021 +0900
@@ -4,7 +4,7 @@
 open import cat-utility
 open import HomReasoning
 open import Data.List hiding ( [_] )
-module ToposIL   {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A)   where
+module ToposIL   {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A)  (n : ToposNat A (CCC.１ c))  where
 
   open Topos
   open Equalizer
@@ -115,62 +115,67 @@
      tl01 : {a b : Obj A}  (p q : Poly a  (Topos.Ω t) b ) 
         → p ⊢ q → q ⊢ p →  A [ Poly.f p ≈ Poly.f q ]
      tl01 {a} {b} p q p<q q<p = begin
-          Poly.f p ≈↑⟨ {!!}  ⟩
-          char t ((equalizer (Ker t (Poly.f p)) ∙  pk ) ∙ qk ) {!!} ≈⟨  {!!}  ⟩
-          char t ((equalizer (Ker t (Poly.f q)) ∙  qk ) ∙ pk ) {!!} ≈⟨  {!!}  ⟩
-          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  ] 
-        qm h = q<p h
-        pp : Hom A b (Topos.Ω t)
-        pp =  Poly.f q
+          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 ⟩
+          Poly.f q ∎   where
         open import equalizer using ( monic )
-        pqiso : Iso A (equalizer-c (Ker t (Poly.f p))) (equalizer-c (Ker t (Poly.f q)))
-        pqiso = equalizer.equ-iso ( isEqualizer (Ker t (Poly.f p))) {!!} -- (isEqualizer (Ker t (Poly.f q)))
-        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))) 
-        eeq :  A [ A [ Poly.f p o equalizer (Ker t (Poly.f q)) ] ≈ A [ A [ ⊤ t o ○ b ] o equalizer (Ker t (Poly.f q)) ] ]
+        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 (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 ⟩
+           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 ⟩
            ⊤ t ∙ ( ○ b ∙  equalizer (Ker t (Poly.f q) ))  ≈⟨ assoc ⟩
            (⊤ t ∙ ○ b) ∙  equalizer (Ker t (Poly.f q) )  ∎  where
-        pk : Hom A (equalizer-c (Ker t (Poly.f q))) (equalizer-c (Ker t (Poly.f p)))
-        pk = IsEqualizer.k (isEqualizer (Ker t (Poly.f p))) (equalizer (Ker t (Poly.f q))) eeq 
-        epq : A [ equalizer (Ker t (Poly.f p)) ∙
-           IsEqualizer.k (Equalizer.isEqualizer (Ker t (Poly.f p))) (equalizer (Ker t (Poly.f q  ))) eeq 
+        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 = IsEqualizer.ek=h (Equalizer.isEqualizer (Ker t (Poly.f p))) 
-        eep :  A [ A [ Poly.f q o equalizer (Ker t (Poly.f p)) ] ≈ A [ A [ ⊤ t o ○ b ] o equalizer (Ker t (Poly.f p)) ] ]
+        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 (Ker t (Poly.f p)) ≈⟨ p<q _ ( begin
-            Poly.f p ∙ equalizer (Ker t (Poly.f p)) ≈⟨ fp ⟩
-            ( ⊤ t ∙ ○ b ) ∙ equalizer (Ker t (Poly.f p)) ≈↑⟨ assoc ⟩
-            ⊤ t ∙ ( ○ b  ∙ equalizer (Ker t (Poly.f p))) ≈⟨ cdr e2 ⟩
-            ⊤ t ∙ ○ (equalizer-c (Ker t (Poly.f p)))  ∎ ) ⟩
-           ⊤ t ∙ ○ (equalizer-c (Ker t (Poly.f p))) ≈↑⟨ cdr e2 ⟩
-           ⊤ t ∙ ( ○ b ∙  equalizer (Ker t (Poly.f p) ))  ≈⟨ assoc ⟩
-           (⊤ t ∙ ○ b) ∙  equalizer (Ker t (Poly.f p) )  ∎  where
-        qk : Hom A (equalizer-c (Ker t (Poly.f p))) (equalizer-c (Ker t (Poly.f q)))
-        qk = IsEqualizer.k (isEqualizer (Ker t (Poly.f q))) (equalizer (Ker t (Poly.f p))) eep 
-        eqp : A [ equalizer (Ker t (Poly.f q)) ∙
-           IsEqualizer.k (Equalizer.isEqualizer (Ker t (Poly.f q))) (equalizer (Ker t (Poly.f p  ))) eep 
-              ≈ equalizer (Ker t (Poly.f p  ))  ]
-        eqp = IsEqualizer.ek=h (Equalizer.isEqualizer (Ker t (Poly.f q))) 
-        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 ]
+           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 } 
+        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} 
 
   module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A) (il : InternalLanguage  Ω ⊤ P) (t : Topos A c) where
diff -r 2755bac8d8b9 -r 10b4d04b734f src/cat-utility.agda
--- a/src/cat-utility.agda	Sun May 09 00:20:48 2021 +0900
+++ b/src/cat-utility.agda	Sun May 09 16:52:27 2021 +0900
@@ -24,6 +24,8 @@
 
         ≡-iso : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (x : Obj C ) → Iso C x x
         ≡-iso C x = record { ≅→ = id1 C _ ; ≅← = id1 C _ ; iso→  = ≈-Reasoning.idL C ; iso←  =  ≈-Reasoning.idL C }
+        sym-iso : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) {x y : Obj C } → Iso C x y → Iso C y x
+        sym-iso C i = record { ≅→ = Iso.≅← i  ; ≅← = Iso.≅→ i ; iso→  = Iso.iso← i ; iso←  =  Iso.iso→ i }
 
         record IsUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                          ( U : Functor B A )