Mercurial > hg > Members > kono > Proof > category

changeset 1025:49fbc57ea772

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Mar 2021 19:55:41 +0900
parents 447bbacacf64
children 7916bde5e57b
files src/CCCSets.agda
diffstat 1 files changed, 51 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Sun Mar 28 08:11:58 2021 +0900
+++ b/src/CCCSets.agda	Mon Mar 29 19:55:41 2021 +0900
@@ -108,6 +108,10 @@
 
 ¬f≡t  : { c : Level } → ¬ (false {c} ≡ true )
 ¬f≡t ()
+
+¬x≡t∧x≡f  : { c : Level } → {x : Bool {c}} → ¬ ((x ≡ false) /\ (x ≡ true) )
+¬x≡t∧x≡f {_} {true} p = ⊥-elim (¬f≡t (sym (proj₁ p)))
+¬x≡t∧x≡f {_} {false} p = ⊥-elim (¬f≡t (proj₂ p))
      
 data _∨_ {c c' : Level } (a : Set c) (b : Set c') : Set (c ⊔ c') where
     case1 : a → a ∨ b
@@ -156,27 +160,60 @@
         tchar {a} {b} m mono y with lem (image m y )
         ... | case1 t = true
         ... | case2 f = false
+        tcharImg : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → (y : a) → tchar m mono y ≡ true → image m y
+        tcharImg  m mono y eq with lem (image m y)
+        ... | case1 t = t
+        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
+        img-x : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → {y : a} → image m y → b
+        img-x m {.(m x)} (isImage x) = x
+        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
+        img-x-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') → img-x m s ≡ img-x m t 
+        img-x-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 = refl
+        img-x-cong0 : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → (y : a) → (s t : image m y ) → img-x m s ≡ img-x m t 
+        img-x-cong0 m mono y s t = img-x-cong m mono y y refl s t
         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→  = {!!} ; iso←  = {!!} } ; iso≈L = {!!} } where
+        isol {a} {b} m mono  = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ;
+               iso→  =  Mono.isMono mono (Sets [ b←s o b→s ]) (id1 Sets _) ( extensionality Sets ( λ x → iso1 x ))
+             ; iso←  =  extensionality Sets ( λ x → iso2 x) } ; iso≈L = {!!} } where
           b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true))
-          b→s x with lem (image m (m x) )
-          ... | case1 x₁ = bs1 x₁ refl where
-             bs1 : {y : a } → image m y → y ≡ m x  → sequ a Bool (λ y → tchar m mono y) (λ _ → true)
-             bs1 (isImage x) eq = elem (m x) {!!}
-          ... | case2 n = ⊥-elim (n (isImage x))
+          b→s x with tchar m mono (m x) | inspect (tchar m mono ) (m x)
+          ... | true | record { eq = eq1 } = elem (m x) eq1
+          b→s x  | false | record { eq = eq1 }  with tchar¬Img m mono (m x) eq1
+          ... | t = ⊥-elim (t (isImage x)) 
           b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b
-          b←s (elem y eq) with lem (image m y)
-          ... | case1 (isImage x) = x
-          ... | case2 t = ⊥-elim ( ¬f≡t eq )
+          b←s (elem y eq) with tchar m mono y | inspect (tchar m mono ) y
+          ... | true | record { eq = eq1 } = img-x m (tcharImg m mono y eq1 )
+          bs=x : (x : b) → (y : a) → y ≡ m x → (eq : tchar m mono y ≡ true ) →  b←s (elem y eq) ≡ x
+          bs=x x y refl t with tcharImg m mono y t
+          ... | t1 = {!!}
+          iso1 : (x : b) → ( Sets [ m o (Sets Category.o b←s) b→s ] ) x ≡  ( Sets [ m o Category.Category.Id Sets ] ) x
+          iso1 x with  tchar m mono (m x) | inspect (tchar m mono ) (m x)
+          ... | true | record { eq = eq1 }  = begin
+             m ( b←s ( elem (m x) eq1 ))  ≡⟨⟩
+             m (img-x m  (isImage (b←s ( elem (m x) eq1 )) )) ≡⟨ {!!} ⟩
+             m (img-x m  (tcharImg m mono (m x) eq1 ) ) ≡⟨ {!!} ⟩
+             m (img-x m  (isImage x) ) ≡⟨⟩
+             m 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) = {!!}
         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) →
                tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y
-        uniq {a} {b} h m mono y with h y  | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y
-        ... | true | case1 x | record { eq = eq1 } = eq1 
-        ... | true | case2 x | record { eq = eq1 } = {!!}
-        ... | false | case1 (isImage (elem x eq)) | record { eq = eq1 } = {!!}
-        ... | false | case2 x | record { eq = eq1 }  = eq1
+        uniq {a} {b} h m mono y with h y  | inspect h y | lem (image (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y
+        ... | true  | record { eq = eqhy } | case1 x | record { eq = eq1 } = eq1 
+        ... | true  | record { eq = eqhy } | case2 x | record { eq = eq1 } = ⊥-elim (x (isImage (elem y eqhy)))
+        ... | false | record { eq = eqhy } | case1 (isImage (elem x eq)) | record { eq = eq1 } = ⊥-elim ( ¬x≡t∧x≡f record {fst = eqhy ; snd = eq })
+        ... | false | record { eq = eqhy } | case2 x | record { eq = eq1 } = eq1
            
 
 open import graph