Mercurial > hg > Members > kono > Proof > category
changeset 1075:10b4d04b734f
fix topos char iso
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 09 May 2021 16:52:27 +0900 |
| parents | 2755bac8d8b9 |
| children | 5e89bbb4cf53 |
| files | src/CCC.agda src/CCCSets.agda src/ToposIL.agda src/cat-utility.agda |
| diffstat | 4 files changed, 83 insertions(+), 75 deletions(-) [+] |
line wrap: on
line diff
--- 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) ⟩
--- 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
--- 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
--- 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 )