Mercurial > hg > Members > kono > Proof > category
changeset 973:5f76e5cf3d49
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 28 Feb 2021 17:31:13 +0900 |
| parents | e05eb6029b5b |
| children | 5731ffd6cf7a |
| files | src/CCC.agda src/ToposEx.agda |
| diffstat | 2 files changed, 24 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCC.agda Sat Feb 27 22:57:42 2021 +0900 +++ b/src/CCC.agda Sun Feb 28 17:31:13 2021 +0900 @@ -169,8 +169,8 @@ (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (○ 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 } (m : Hom A b a ) → ( mono : Mono A m ) → {h : Hom A a Ω} + → 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 @@ -182,6 +182,8 @@ isTopos : IsTopos A １ ○ Ω ⊤ 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 ) } record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field
--- a/src/ToposEx.agda Sat Feb 27 22:57:42 2021 +0900 +++ b/src/ToposEx.agda Sun Feb 28 17:31:13 2021 +0900 @@ -101,6 +101,9 @@ id1 A _ o g ≈⟨ idL ⟩ g ∎ + open Equalizer + open import equalizer + prop32→ : {a b : Obj A}→ (f g : Hom A a b ) → A [ f ≈ g ] → A [ A [ char t < id1 A b , id1 A b > δmono o < f , g > ] ≈ A [ ⊤ t o ○ a ] ] prop32→ {a} {b} f g f=g = begin @@ -108,10 +111,25 @@ 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 _ , id1 A _ > ) o f ≈⟨ {!!} ⟩ + (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) o f ≈⟨ car lem1 ⟩ (⊤ t o ○ b) o f ≈↑⟨ assoc ⟩ ⊤ t o (○ b o f) ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ - ⊤ t o ○ a ∎ + ⊤ t o ○ a ∎ where + i = char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > + e = Ker t ( ⊤ t o ○ b) + ki = IsEqualizer.k (isEqualizer e) (id1 A _) refl-hom + lem1 : (char t < id1 A b , id1 A b > δmono o < id1 A _ , id1 A _ > ) ≈ ( ⊤ t o ○ b ) + lem1 = begin + i ≈↑⟨ idR ⟩ + i o id1 A _ ≈↑⟨ cdr (IsEqualizer.ek=h (isEqualizer e) ) ⟩ + i o (equalizer e o ki ) ≈⟨ assoc ⟩ + (i o equalizer e ) o ki ≈⟨ {!!} ⟩ + (((⊤ t) o (○ b)) o equalizer e ) o ki ≈⟨ car (IsEqualizer.fe=ge (isEqualizer e)) ⟩ + ((⊤ t o ○ b) o equalizer e ) o ki ≈↑⟨ assoc ⟩ + (⊤ t o ○ b) o (equalizer e o ki ) ≈⟨ cdr (IsEqualizer.ek=h (isEqualizer e) )⟩ + (⊤ t o ○ b) o id1 A _ ≈⟨ idR ⟩ + ⊤ t o ○ b ∎ + 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 ]