Mercurial > hg > Members > kono > Proof > category
changeset 1074:2755bac8d8b9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 09 May 2021 00:20:48 +0900 |
| parents | 785d8b2ba48f |
| children | 10b4d04b734f |
| files | src/CCC.agda src/ToposIL.agda src/equalizer.agda |
| diffstat | 3 files changed, 46 insertions(+), 29 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCC.agda Sat May 08 19:02:57 2021 +0900 +++ b/src/CCC.agda Sun May 09 00:20:48 2021 +0900 @@ -181,23 +181,6 @@ ≈ subst (λ k → Hom B k (FObj functor a)) (trans (cong (λ k → CCC._∧_ cb k (FObj functor b)) (sym f<=)) (sym f∧)) (CCC.ε cb {FObj functor a} {FObj functor b}) ] ----- --- --- Sub Object Classifier as Topos --- pull back on --- --- iso ○ b --- e ⇐====⇒ b -----------→ 1 m ∙ f ≈ m ∙ g → f ≈ g --- | | | --- | m | | ⊤ --- | ↓ char m ↓ Ker h = Equalizer (char m mono) (⊤ ∙ ○ a ) --- + ------→ a -----------→ Ω m = Equalizer (char m mono) (⊤ ∙ ○ a ) --- ker h h --- --- if m is an equalizer, there is an iso between e and b as k, and if we have the iso, m becomes an equalizer. --- equalizer.equalizerIso : {a b c : Obj A} → (f g : Hom A a b ) → (equ : Equalizer A f g ) --- → (m : Hom A c a) → ( ker-iso : IsoL A m (equalizer equ) ) → IsEqualizer A m f g - open Equalizer open import equalizer @@ -239,6 +222,23 @@ if=ig : ( m o Iso.≅→ i ) o f ≈ ( m o Iso.≅→ i ) o g → m o (Iso.≅→ i o f ) ≈ m o ( Iso.≅→ i o g ) if=ig eq = trans-hom assoc (trans-hom eq (sym-hom assoc ) ) +---- +-- +-- Sub Object Classifier as Topos +-- pull back on +-- +-- iso ○ b +-- e ⇐====⇒ b -----------→ 1 m ∙ f ≈ m ∙ g → f ≈ g +-- | | | +-- | m | | ⊤ +-- | ↓ char m ↓ Ker h = Equalizer (char m mono) (⊤ ∙ ○ a ) +-- + ------→ a -----------→ Ω m = Equalizer (char m mono) (⊤ ∙ ○ a ) +-- ker h h +-- +-- if m is an equalizer, there is an iso between e and b as k, and if we have the iso, m becomes an equalizer. +-- equalizer.equalizerIso : {a b c : Obj A} → (f g : Hom A a b ) → (equ : Equalizer A f g ) +-- → (m : Hom A c a) → ( ker-iso : IsoL A m (equalizer equ) ) → IsEqualizer A m f g + record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) ( Ω : Obj A ) ( ⊤ : Hom A (CCC.１ c) Ω )
--- a/src/ToposIL.agda Sat May 08 19:02:57 2021 +0900 +++ b/src/ToposIL.agda Sun May 09 00:20:48 2021 +0900 @@ -115,13 +115,9 @@ 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 ≈↑⟨ tt p ⟩ - char t (equalizer (Ker t (Poly.f p))) (mm p) ≈↑⟨ IsTopos.char-iso (Topos.isTopos t) {!!} {!!} ⟩ - char t (equalizer (Ker t (Poly.f p)) ∙ {!!} ) {!!} ≈⟨ {!!} ⟩ - char t {!!} {!!} ≈⟨ IsTopos.char-iso (Topos.isTopos t) {!!} {!!} ⟩ - char t (equalizer (Ker t (Poly.f p)) - ∙ IsEqualizer.k (isEqualizer (Ker t (Poly.f p))) (equalizer (Ker t (Poly.f q))) ee1) {!!} ≈⟨ IsTopos.char-cong (Topos.isTopos t) ee ⟩ - char t (equalizer (Ker t (Poly.f q))) (mm q) ≈⟨ tt q ⟩ + 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) @@ -134,12 +130,14 @@ pp : Hom A b (Topos.Ω t) pp = Poly.f q 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))) - ee1 : A [ A [ Poly.f p o equalizer (Ker t (Poly.f q)) ] ≈ A [ A [ ⊤ t o ○ b ] o equalizer (Ker t (Poly.f q)) ] ] - ee1 = begin + 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)) ] ] + 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 ⟩ @@ -148,10 +146,28 @@ ⊤ t ∙ ○ (equalizer-c (Ker t (Poly.f q))) ≈↑⟨ cdr e2 ⟩ ⊤ t ∙ ( ○ b ∙ equalizer (Ker t (Poly.f q) )) ≈⟨ assoc ⟩ (⊤ t ∙ ○ b) ∙ equalizer (Ker t (Poly.f q) ) ∎ where - ee : A [ equalizer (Ker t (Poly.f p)) ∙ - IsEqualizer.k (Equalizer.isEqualizer (Ker t (Poly.f p))) (equalizer (Ker t (Poly.f q ))) ee1 + 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 ≈ equalizer (Ker t (Poly.f q )) ] - ee = IsEqualizer.ek=h (Equalizer.isEqualizer (Ker t (Poly.f p))) + 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)) ] ] + 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 ]