# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1621319926 -32400
# Node ID 0211d99f29fc616a9b2012a93ecaac3302be0a42
# Parent  bcaa8f66ec09a0d22da154a163c79c3d5e780edb
Topos Sets char-iso done

diff -r bcaa8f66ec09 -r 0211d99f29fc src/CCC.agda
--- a/src/CCC.agda	Tue May 18 01:06:43 2021 +0900
+++ b/src/CCC.agda	Tue May 18 15:38:46 2021 +0900
@@ -251,11 +251,16 @@
          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-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-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 ]
+                (i : Iso A a a' ) → A [ p ≈ A [ q o Iso.≅→ i ] ]  → 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 _)
+     char-cong {a} {b} {m} {m'} {mo} {mo'} m=m' = char-iso m m' mo mo' (≡-iso A _) ( begin 
+            m ≈⟨ m=m' ⟩
+            m' ≈↑⟨ idR  ⟩
+            m' o Iso.≅→ (≡-iso A b) ∎ ) 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 ] ]
diff -r bcaa8f66ec09 -r 0211d99f29fc src/CCCSets.agda
--- a/src/CCCSets.agda	Tue May 18 01:06:43 2021 +0900
+++ b/src/CCCSets.agda	Tue May 18 15:38:46 2021 +0900
@@ -250,8 +250,8 @@
               ; iso←  =  extensionality Sets ( λ x → iso2 x) } 
 
         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 = extensionality Sets (λ y → iso-m1 y ) where
+            (i : Iso Sets a a' ) → Sets [ p ≈ Sets [ q o Iso.≅→ i ] ] → Sets [ tchar p mp ≈ tchar q mq ]
+        iso-m {a} {a'} {b} p q mp mq i ei = extensionality Sets (λ y → iso-m1 y ) where
            --
            --          Iso.≅← i     x      ○ a            mq : q ( f x ) ≡ q ( g x ) → f x ≡ g x 
            --       a'------------→ a -----------→ 1
@@ -265,16 +265,18 @@
            iso-m1 y with lem (image p y) | lem (image q y) 
            ... | case1 (isImage x) |  case1 x₁  = refl
            ... | case1 (isImage x) |  case2 not = ⊥-elim ( not iso-m2 ) where
-               iso-m3 : image p y  --    → p x ≣ y
-               iso-m3 = isImage x
                iso-m4 :  q ( Iso.≅→ i x ) ≡ p x
                iso-m4 = begin
-                  q ( Iso.≅→ i x )  ≡⟨ {!!} ⟩
-                  p ( Iso.≅← i ( Iso.≅→ i x)  )  ≡⟨ {!!} ⟩
+                  q ( Iso.≅→ i x )  ≡⟨ sym ( cong ( λ k → k x) ei ) ⟩
                   p x ∎ where open ≡-Reasoning
                iso-m2 : image q (p x)   
                iso-m2 = subst (λ k → image q k) iso-m4 ( isImage ( Iso.≅→ i x ) ) 
-           ... | case2 x |  case1 (isImage x₁) = {!!}
+           ... | case2 not |  case1 (isImage x) = ⊥-elim ( not ( subst (λ k → image p k) iso-m3 ( isImage ( Iso.≅← i x ) ) )) where
+               iso-m3 :  p (Iso.≅← i x) ≡ q x
+               iso-m3 = begin
+                  p (Iso.≅← i x)  ≡⟨  cong ( λ k → k (Iso.≅← i x) ) ei ⟩
+                  q (Iso.≅→ i (Iso.≅← i x))  ≡⟨ cong (λ k → q k) (cong (λ k1 → k1 x) (Iso.iso← i)) ⟩
+                  q x ∎ where open ≡-Reasoning
            ... | case2 x |  case2 not = refl
 
         open import Polynominal (Sets {c} )  (sets {c})
diff -r bcaa8f66ec09 -r 0211d99f29fc src/ToposIL.agda
--- a/src/ToposIL.agda	Tue May 18 01:06:43 2021 +0900
+++ b/src/ToposIL.agda	Tue May 18 15:38:46 2021 +0900
@@ -92,7 +92,7 @@
       ;  _∈_ = λ {a} x α →  A [ ε o < α , x > ]
       -- { x ∈ a | φ x } : P a
       ;  select = λ {a} φ →  Fc.g ( fc t φ )
-      ;  apply = λ {a}  φ x → record { x = x ; f = Functional-completeness.fun (fc0 t φ ) ∙ < x ∙  ○ _ , id1 A _ >  ; phi = i ; idx = Poly.idx φ }
+      ;  apply = λ {a}  φ x → record { x = x ; f = Functional-completeness.fun (fc0 t φ ) ∙ < x ∙  ○ _ , id1 A _ >  ; phi = i _ ; nf = {!!} }
       ;  isIL = record {
            isSelect = {!!}
          ; uniqueSelect = {!!}
@@ -117,7 +117,7 @@
         → 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 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 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 ei ⟩
           char t (equalizer (kp q) ) (eMonic A (kp q)) ≈⟨ tt q ⟩
           Poly.f q ∎   where
         open import equalizer using ( monic )
@@ -148,6 +148,8 @@
            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  } 
+        ei :  A [ equalizer (Ker t (Poly.f p)) ≈ A [ equalizer (Ker t (Poly.f q)) o Iso.≅→ pqiso ] ]
+        ei = sym (ek=h (isEqualizer (kp q)) )
         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}