Mercurial > hg > Members > kono > Proof > category

changeset 1016:bbbe97d2a5ea

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 Tue, 23 Mar 2021 14:41:47 +0900
parents e01a1d29492b
children 90224a662c4e
files src/CCC.agda src/CCCSets.agda src/Polynominal.agda src/ToposEx.agda
diffstat 4 files changed, 38 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Sun Mar 21 10:16:57 2021 +0900
+++ b/src/CCC.agda	Tue Mar 23 14:41:47 2021 +0900
@@ -184,13 +184,14 @@
 --
 -- Sub Object Classifier as Topos
 -- pull back on
---             ○ b
---       b -----------→ 1
---       |              |
---     m |              | ⊤
---       ↓    char m    ↓
---       a -----------→ Ω
---             h
+--
+--     iso          ○ b
+--  e ⇐====⇒  b -----------→ 1
+--  |         |              |
+--  |       m |              | ⊤
+--  |         ↓    char m    ↓
+--  + ------→ a -----------→ Ω
+--     ker h        h
 --
 open Equalizer
 open import equalizer
@@ -201,6 +202,8 @@
 
 open Mono
 
+open import equalizer
+
 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) 
         ( Ω : Obj A )
         ( ⊤ : Hom A (CCC.１ c) Ω )
@@ -208,8 +211,27 @@
         (char : {a b : Obj A} → (m :  Hom A b a) → Mono A m  → Hom A a Ω) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
          char-uniqueness  : {a b : Obj A } {h : Hom A a Ω}  (m :  Hom A b a) → (mono : Mono A m)  
-             → A [ char m mono  ≈ h ]
+             → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
          ker-iso : {a b : Obj A} →  (m :  Hom A b a) → (mono : Mono A m)  → IsoL A m (equalizer (Ker ( char m mono ))) 
+     ker : {a : Obj A} → ( h : Hom A a Ω )  → Hom A ( equalizer-c (Ker h) ) a
+     ker h = equalizer (Ker h)
+     mm : {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m ) → A [ A [ equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ] ≈  m ]
+     mm m mono = IsoL.L≈iso  (ker-iso m mono)
+     mequ : {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m ) → Equalizer A (char m mono)  (A [ ⊤ o (CCC.○ c a) ])
+     mequ {a} {b} m mono = record { equalizer-c = b ; equalizer = m ; isEqualizer = 
+            subst (λ k → IsEqualizer A k _ _ ) {!!} -- 
+              ( equalizer+iso (Ker (char m mono)) (Iso.≅→ (IsoL.iso-L (ker-iso m mono)))
+                 (Iso.≅← (IsoL.iso-L (ker-iso m mono))) (Iso.iso→ (IsoL.iso-L (ker-iso m mono))) (Iso.iso← (IsoL.iso-L (ker-iso m mono))) ) }
+     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 ≈⟨ {!!} ⟩
+            char (ker (char m mono) ) {!!} o m ≈⟨ {!!} ⟩
+            char m mono  o (ker (char m mono) o Iso.≅→ (IsoL.iso-L (ker-iso m mono))) ≈⟨ {!!} ⟩
+            (char m mono  o ker (char m mono) ) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ≈⟨ {!!} ⟩
+            {!!} ≈⟨ {!!} ⟩
+            (⊤ o  CCC.○ c a) o m ≈↑⟨ assoc ⟩
+            ⊤ o  (CCC.○ c a o m ) ≈⟨ cdr (IsCCC.e2 (CCC.isCCC c)) ⟩
+            ⊤ o CCC.○ c b  ∎  where   open ≈-Reasoning A
 
 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  (c : CCC A)  :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
@@ -218,16 +240,8 @@
          Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ])
          char : {a b : Obj A} → (m : Hom A b a ) → Mono A m → Hom A a Ω
          isTopos : IsTopos A c Ω ⊤ Ker char
-     ker : {a : Obj A} → ( h : Hom A a Ω )  → Hom A ( equalizer-c (Ker h) ) a
-     ker h = equalizer (Ker h)
      Monik : {a : Obj A} (h : Hom A a Ω)  → Mono A (equalizer (Ker h))
      Monik h = record { isMono = λ f g → monic (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 ] ]
-     char-m=⊤ {a} {b} m mono  = begin
-            char m mono  o m ≈⟨ car (IsTopos.char-uniqueness isTopos m mono) ⟩
-            (⊤ o  CCC.○ c a) o m ≈↑⟨ assoc ⟩
-            ⊤ o  (CCC.○ c a o m ) ≈⟨ cdr (IsCCC.e2 (CCC.isCCC c)) ⟩
-            ⊤ o CCC.○ c b  ∎  where   open ≈-Reasoning A
 
 record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
--- a/src/CCCSets.agda	Sun Mar 21 10:16:57 2021 +0900
+++ b/src/CCCSets.agda	Tue Mar 23 14:41:47 2021 +0900
@@ -121,7 +121,7 @@
       ;  Ker = tker
       ;  char = tchar
       ;  isTopos = record {
-                 char-uniqueness  = λ {a} {b} {h} m mono →  extensionality Sets ( λ x → uniq h m mono x )
+                 char-uniqueness  = λ {a} {b} {h} m mono →  {!!} -- extensionality Sets ( λ x → uniq h m mono x )
               ;  ker-iso = {!!}
          }
     } where
@@ -161,10 +161,12 @@
         uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (x : a) → true ≡ h x
         uniq {a} {b} h m mono x = begin
             true ≡⟨⟩
-            (λ × → true ) x ≡⟨ {!!} ⟩
-            {!!} ≡⟨ cong (λ k → h (k x)  ) (IsEqualizer.ek=h (Equalizer.isEqualizer (tker h)) {{!!}} {{!!}} )  ⟩
+            (λ × → true ) x ≡⟨ cong (λ k → {!!} ) (sym (IsEqualizer.fe=ge (Equalizer.isEqualizer (tker h)) ) ) ⟩
+            {!!} ≡⟨  {!!} ⟩
             h x  ∎  where
               open ≡-Reasoning 
+              yy : Sets [ (λ e → {!!} ) ≈ (λ e → true) ] 
+              yy = IsEqualizer.fe=ge (Equalizer.isEqualizer (tker h))
               yyy : {c : Obj Sets } → (f g : c → b ) → Sets [ Sets [ m o f ] ≈ Sets [ m o g ] ] → f ≡ g
               yyy f g eq = Mono.isMono mono f g eq
               yyy1 : {c : Obj Sets } → (f g : c → b ) → Sets [ Sets [ m o f ] ≈ Sets [ m o g ] ] → f ≡ g
--- a/src/Polynominal.agda	Sun Mar 21 10:16:57 2021 +0900
+++ b/src/Polynominal.agda	Tue Mar 23 14:41:47 2021 +0900
@@ -254,6 +254,7 @@
               f ∙  < π , π' >  ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
               f ∙  id1 A _ ≈⟨ idR ⟩
               f ∎  ) where
+          -- fc1 may be wrong. is should be a field of PHom, and  k x {x ∙ ○ b} i may be proved standalone.
           fc1 : {b c : Obj A} (p : PHom b c) → A [ k x (phi p)  ≈ k x {hom p} i ]    -- it looks like (*) in page 60
           fc1 {b} {c} p = uniq record { hom =  hom p ; phi = i }  ( k x (phi p)) ( begin -- non terminating because of the record, which we may avoid
                k x (phi p) ∙ < x ∙ ○ b , id1 A b > ≈⟨ fc0 p ⟩
--- a/src/ToposEx.agda	Sun Mar 21 10:16:57 2021 +0900
+++ b/src/ToposEx.agda	Tue Mar 23 14:41:47 2021 +0900
@@ -77,7 +77,7 @@
     ; π1 = m    
     ; π2 = ○ b   
     ; isPullback = record {
-              commute = char-m=⊤ t m mono
+              commute = ? -- char-m=⊤ t m mono
          ;    pullback = λ {d} {p1} {p2} eq →  f← o k  p1 p2 eq
          ;    π1p=π1 = λ {d} {p1'} {p2'} {eq} → lemma3 p1' p2' eq
          ;    π2p=π2 = λ {d} {p1'} {p2'} {eq} → trans-hom (IsCCC.e2 isCCC) (sym (IsCCC.e2 isCCC))
@@ -149,7 +149,7 @@
             char t < id1 A b , id1 A b > δmono o < f , f >  ≈↑⟨ cdr ( IsCCC.π-cong isCCC idL idL ) ⟩
             char t < id1 A b , id1 A b > δmono o < id1 A _ o f , id1 A _ o f >    ≈↑⟨ cdr ( IsCCC.distr-π isCCC ) ⟩
             char t < id1 A b , id1 A b > δmono o (< id1 A _ , id1 A _ > o f)   ≈⟨ assoc ⟩
-           (char t < id1 A b , id1 A b > δmono o < id1 A b , id1 A b > ) o f  ≈⟨ car (char-m=⊤ t < id1 A b , id1 A b > δmono  ) ⟩
+           (char t < id1 A b , id1 A b > δmono o < id1 A b , id1 A b > ) o f  ≈⟨ car ? ⟩
             (⊤ t o  ○  b)  o f  ≈↑⟨ assoc ⟩
             ⊤ t o  (○  b  o f)  ≈⟨ cdr (IsCCC.e2 isCCC)  ⟩
             ⊤ t o  ○  a  ∎