Mercurial > hg > Members > kono > Proof > category

changeset 1032:c3b3faa791fa sets-topos

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
topos of Sets done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Mar 2021 23:30:55 +0900
parents 52c98490c877
children a59c51b541a2
files src/CCCSets.agda src/SetsCompleteness.agda
diffstat 2 files changed, 32 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Tue Mar 30 20:22:20 2021 +0900
+++ b/src/CCCSets.agda	Tue Mar 30 23:30:55 2021 +0900
@@ -160,13 +160,14 @@
         tchar {a} {b} m mono y with lem (image m y )
         ... | case1 t = true
         ... | case2 f = false
+
         open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
         img-cong : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (y y' : a) → y ≡ y' → (s : image m y ) (t : image m y') → s ≅ t
         img-cong {a} {b} m mono .(m x) .(m x₁) eq (isImage x) (isImage x₁)
             with cong (λ k → k ! ) ( Mono.isMono mono {One} (λ _ → x) (λ _ → x₁ ) ( extensionality Sets ( λ _ → eq )) )
         ... | refl = HE.refl
-        image-iso : {a b : Obj (Sets {c})} (m : Hom Sets b a) → (mono : Mono Sets m )  (y : a) → (i0 i1 : image m y ) → i0 ≡ i1
-        image-iso {a} {b} m mono y i0 i1 = HE.≅-to-≡ (img-cong m mono y y refl i0 i1)
+        image-uniq : {a b : Obj (Sets {c})} (m : Hom Sets b a) → (mono : Mono Sets m )  (y : a) → (i0 i1 : image m y ) → i0 ≡ i1
+        image-uniq {a} {b} m mono y i0 i1 = HE.≅-to-≡ (img-cong m mono y y refl i0 i1)
         tchar¬Img : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  (y : a) → tchar m mono y ≡ false → ¬ image m y
         tchar¬Img  m mono y eq im with lem (image m y) 
         ... | case2 n  = n im
@@ -174,6 +175,8 @@
         b2i m x = isImage x
         i2b : {a b : Obj (Sets {c}) } (m : Hom Sets b a) →  {y : a} → image m y → b
         i2b m (isImage x) = x
+        img-mx=y :  {a b : Obj (Sets {c}) } (m : Hom Sets b a) →  {y : a} → (im : image m y ) → m (i2b m im) ≡ y
+        img-mx=y m (isImage x) = refl
         b2i-iso : {a b : Obj (Sets {c}) } (m : Hom Sets b a) →  (x : b) → i2b m (b2i m x) ≡ x
         b2i-iso m x = refl
         b2s : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) →  sequ a Bool (tchar m mono)  (λ _ → true )
@@ -184,30 +187,46 @@
         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
-        s2ii : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (x : b) → (eq1 : tchar m mono (m x)  ≡ true)
-            → s2i m mono (elem (m x ) eq1) ≡ isImage x
-        s2ii m mono x eq1 with lem (image m (m x))
-        ... | case1 im = s2ii0 where
-            s2ii0 :  im ≡ isImage x
-            s2ii0 = image-iso m mono (m x) im (isImage x)
         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 = {!!} } where
+             ; iso←  =  extensionality Sets ( λ x → iso2 x) } ; iso≈L = extensionality Sets ( λ s → iso3 s ) } 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
           b←s (elem y eq) = i2b m (s2i m mono (elem y eq))
+          iso3 : (s : sequ a Bool (tchar m mono) (λ _ → true)) → m (b←s s) ≡ equ s
+          iso3 (elem y eq) with lem (image m y)
+          ... | case1 (isImage x) = refl
           iso1 : (x : b) → b←s ( b→s x ) ≡  x
           iso1 x with  tchar m mono (m x) | inspect (tchar m mono ) (m x)
           ... | true | record { eq = eq1 }  = begin
              b←s ( elem (m x) eq1 )  ≡⟨⟩
-             i2b m (s2i m mono (elem (m x ) eq1 ))  ≡⟨ cong (λ k → i2b m k) (s2ii m mono x eq1 ) ⟩
+             i2b m (s2i m mono (elem (m x ) eq1 ))  ≡⟨ cong (λ k → i2b m k) (image-uniq m mono (m x) (s2i m mono (elem (m x ) eq1 )) (isImage x) ) ⟩
              i2b m (isImage x)  ≡⟨⟩
              x ∎ where open ≡-Reasoning
           iso1 x | false | record { eq = eq1 } = ⊥-elim ( tchar¬Img m mono (m x) eq1 (isImage x))
           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) = {!!}
+          iso2 (elem y eq) = begin
+             b→s ( b←s (elem y eq)) ≡⟨⟩
+             b2s m mono ( i2b m (s2i m mono (elem y eq)))  ≡⟨⟩
+             b2s m mono x  ≡⟨ elm-cong _ _ (iso21 x ) ⟩
+             elem (m x) eq1 ≡⟨ elm-cong _ _ mx=y ⟩
+             elem y eq  ∎ where
+               open ≡-Reasoning
+               x : b
+               x = i2b m (s2i m mono (elem y eq))
+               eq1 : tchar m mono (m x) ≡ true
+               eq1 with lem (image m (m x))
+               ... | case1 t = refl
+               ... | case2 n = ⊥-elim (n (isImage x))
+               mx=y : m x ≡ y
+               mx=y = img-mx=y m (s2i m mono (elem y eq))
+               iso21 : (x : b)  → equ (b2s m mono x ) ≡ m x
+               iso21 x with  tchar m mono (m x) | inspect (tchar m mono) (m x)
+               ... | true | record {eq = eq1} = refl
+               ... | false | record { eq = eq1 } with tchar¬Img m mono (m x) eq1
+               ... | t = ⊥-elim (t (isImage x)) 
         imequ   : {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 ])
         imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono)
         uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) →
--- a/src/SetsCompleteness.agda	Tue Mar 30 20:22:20 2021 +0900
+++ b/src/SetsCompleteness.agda	Tue Mar 30 23:30:55 2021 +0900
@@ -166,6 +166,8 @@
 
 irr : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
 irr refl refl = refl
+elm-cong : {  c₂ : Level}  {a b : Set c₂}  {f g : Hom (Sets {c₂}) a b}  (x y : sequ a b f g) → equ x ≡ equ y →  x  ≡ y
+elm-cong ( elem x eq  ) (elem .x eq' ) refl   =  ≡cong ( λ ee → elem x ee ) ( irr eq eq' )
 
 open sequ
 
@@ -187,8 +189,6 @@
            ek=h {d} {h} {eq} = refl
            injection :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} (f  : Hom Sets a b) → Set c₂
            injection f =  ∀ x y  → f x ≡ f y →  x  ≡ y
-           elm-cong :   (x y : sequ a b f g) → equ x ≡ equ y →  x  ≡ y
-           elm-cong ( elem x eq  ) (elem .x eq' ) refl   =  ≡cong ( λ ee → elem x ee ) ( irr eq eq' )
            lemma5 :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x)
            lemma5 refl  x  = refl   -- somehow this is not equal to lemma1