Mercurial > hg > Members > kono > Proof > category
changeset 975:f8fba4f1dcfa
char-m=⊤
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Mar 2021 17:01:00 +0900 |
| parents | 5731ffd6cf7a |
| children | 73fd14a73d49 |
| files | src/CCC.agda src/ToposEx.agda |
| diffstat | 2 files changed, 18 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCC.agda Mon Mar 01 11:26:28 2021 +0900 +++ b/src/CCC.agda Mon Mar 01 17:01:00 2021 +0900 @@ -163,27 +163,33 @@ open Mono -record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) +record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) ( Ω : Obj A ) - ( ⊤ : Hom A １ Ω ) - (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ])) + ( ⊤ : Hom A (CCC.１ c) Ω ) + (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 Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field - char-ker : {a b : Obj A } {h : Hom A a Ω} - → A [ char (equalizer (Ker h)) record { isMono = λ f g → monic (Ker h) } ≈ h ] + char-ker : {a b : Obj A } {h : Hom A a Ω} (m : Hom A b a) → (mono : Mono A m) + → A [ char m mono ≈ h ] ker-char : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → Iso A b ( equalizer-c (Ker ( char m mono ))) -record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (○ : (a : Obj A ) → Hom A a １) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where +record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field Ω : Obj A - ⊤ : Hom A １ Ω - Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ a) ]) + ⊤ : Hom A (CCC.１ c) Ω + 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 １ ○ Ω ⊤ Ker char + 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-ker 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/ToposEx.agda Mon Mar 01 11:26:28 2021 +0900 +++ b/src/ToposEx.agda Mon Mar 01 17:01:00 2021 +0900 @@ -3,7 +3,7 @@ open import Category open import cat-utility open import HomReasoning -module ToposEx {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A (CCC.１ c) (CCC.○ c) ) where +module ToposEx {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) where open Topos open Equalizer @@ -90,13 +90,10 @@ 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 Pullback.π1 pb ) o f ≈⟨ car (IsPullback.commute (Pullback.isPullback pb)) ⟩ + (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 ) ⟩ (⊤ t o ○ b) o f ≈↑⟨ assoc ⟩ ⊤ t o (○ b o f) ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ - ⊤ t o ○ a ∎ where - pb : Pullback A (char t < id1 A b , id1 A b > δmono) (⊤ t ) - pb = {!!} - + ⊤ t o ○ a ∎ prop23→ : {a b : Obj A}→ (f g : Hom A a b ) → A [ A [ char t < id1 A b , id1 A b > δmono o < f , g > ] ≈ A [ ⊤ t o ○ a ] ] → A [ f ≈ g ]