Mercurial > hg > Members > kono > Proof > category
annotate src/ToposEx.agda @ 979:8e97363859ce
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Mar 2021 00:58:24 +0900 |
| parents | db288effad97 |
| children | 8ab4307d9337 |
| rev | line source |
|---|---|
| 963 | 1 open import CCC |
| 2 open import Level | |
| 3 open import Category | |
| 4 open import cat-utility | |
| 5 open import HomReasoning | |
| 975 | 6 module ToposEx {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) where |
| 963 | 7 |
| 974 | 8 open Topos |
| 9 open Equalizer | |
| 10 open ≈-Reasoning A | |
| 11 open CCC.CCC c | |
| 12 | |
| 963 | 13 |
| 14 -- ○ b | |
| 15 -- b -----------→ 1 | |
| 16 -- | | | |
| 17 -- m | | ⊤ | |
| 18 -- ↓ char m ↓ | |
| 19 -- a -----------→ Ω | |
| 20 -- h | |
| 964 | 21 -- |
| 22 -- Ker t h : Equalizer A h (A [ ⊤ o (○ a) ]) | |
| 963 | 23 |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
24 mh=⊤ : {a d : Obj A} (h : Hom A a (Ω t)) (p1 : Hom A d a) (p2 : Hom A d １) (eq : A [ A [ h o p1 ] ≈ A [ ⊤ t o p2 ] ] ) |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
25 → A [ A [ h o p1 ] ≈ A [ A [ ⊤ t o ○ a ] o p1 ] ] |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
26 mh=⊤ {a} {d} h p1 p2 eq = begin |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
27 h o p1 ≈⟨ eq ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
28 ⊤ t o p2 ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
29 ⊤ t o (○ d) ≈↑⟨ cdr (IsCCC.e2 isCCC) ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
30 ⊤ t o ( ○ a o p1 ) ≈⟨ assoc ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
31 (⊤ t o ○ a ) o p1 ∎ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
32 |
| 974 | 33 topos-pullback : {a : Obj A} → (h : Hom A a (Ω t)) → Pullback A h (⊤ t) |
| 34 topos-pullback {a} h = record { | |
| 963 | 35 ab = equalizer-c (Ker t h) -- b |
| 36 ; π1 = equalizer (Ker t h) -- m | |
| 37 ; π2 = ○ ( equalizer-c (Ker t h) ) -- ○ b | |
| 38 ; isPullback = record { | |
| 39 commute = comm | |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
40 ; pullback = λ {d} {p1} {p2} eq → IsEqualizer.k (isEqualizer (Ker t h)) p1 (mh=⊤ h p1 p2 eq ) |
| 964 | 41 ; π1p=π1 = IsEqualizer.ek=h (isEqualizer (Ker t h)) |
| 42 ; π2p=π2 = λ {d} {p1'} {p2'} {eq} → lemma2 eq | |
| 43 ; uniqueness = uniq | |
| 963 | 44 } |
| 974 | 45 } where |
| 46 e2 = IsCCC.e2 isCCC | |
| 963 | 47 comm : A [ A [ h o equalizer (Ker t h) ] ≈ A [ ⊤ t o ○ (equalizer-c (Ker t h)) ] ] |
| 48 comm = begin | |
| 964 | 49 h o equalizer (Ker t h) ≈⟨ IsEqualizer.fe=ge (isEqualizer (Ker t h)) ⟩ |
| 50 (⊤ t o ○ a ) o equalizer (Ker t h) ≈↑⟨ assoc ⟩ | |
| 974 | 51 ⊤ t o (○ a o equalizer (Ker t h)) ≈⟨ cdr e2 ⟩ |
| 963 | 52 ⊤ t o ○ (equalizer-c (Ker t h)) ∎ |
| 964 | 53 lemma2 : {d : Obj A} {p1' : Hom A d a} {p2' : Hom A d １} (eq : A [ A [ h o p1' ] ≈ A [ ⊤ t o p2' ] ] ) |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
54 → A [ A [ ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(mh=⊤ h p1' p2' eq) ] ≈ p2' ] |
| 964 | 55 lemma2 {d} {p1'} {p2'} eq = begin |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
56 ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(mh=⊤ h p1' p2' eq) ≈⟨ e2 ⟩ |
| 964 | 57 ○ d ≈↑⟨ e2 ⟩ |
| 58 p2' ∎ | |
| 976 | 59 uniq : {d : Obj A} (p' : Hom A d (equalizer-c (Ker t h))) (π1' : Hom A d a) (π2' : Hom A d １) (eq : A [ A [ h o π1' ] ≈ A [ ⊤ t o π2' ] ]) |
| 60 (π1p=π1' : A [ A [ equalizer (Ker t h) o p' ] ≈ π1' ]) (π2p=π2' : A [ A [ ○ (equalizer-c (Ker t h)) o p' ] ≈ π2' ]) | |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
61 → A [ IsEqualizer.k (isEqualizer (Ker t h)) π1' (mh=⊤ h π1' π2' eq) ≈ p' ] |
| 976 | 62 uniq {d} (p') p1' p2' eq pe1 pe2 = begin |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
63 IsEqualizer.k (isEqualizer (Ker t h)) p1' (mh=⊤ h p1' p2' eq) ≈⟨ IsEqualizer.uniqueness (isEqualizer (Ker t h)) pe1 ⟩ |
| 964 | 64 p' ∎ |
| 963 | 65 |
| 974 | 66 topos-m-pullback : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono ) (⊤ t) |
| 976 | 67 topos-m-pullback {a} {b} m mono = record { |
| 68 ab = b | |
| 69 ; π1 = m | |
| 70 ; π2 = ○ b | |
| 71 ; isPullback = record { | |
| 72 commute = char-m=⊤ t m mono | |
| 978 | 73 ; pullback = λ {d} {p1} {p2} eq → f← o k p1 p2 eq |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
74 ; π1p=π1 = λ {d} {p1'} {p2'} {eq} → lemma3 p1' p2' eq |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
75 ; π2p=π2 = λ {d} {p1'} {p2'} {eq} → trans-hom (IsCCC.e2 isCCC) (sym (IsCCC.e2 isCCC)) |
| 979 | 76 ; uniqueness = uniq |
| 976 | 77 } |
| 78 } where | |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
79 f← = Iso.≅← (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono )) |
| 978 | 80 f→ = Iso.≅→ (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono )) |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
81 k : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) → A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] → Hom A d (equalizer-c (Ker t (char t m mono))) |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
82 k p1 p2 eq = IsEqualizer.k (isEqualizer (Ker t (char t m mono))) p1 (mh=⊤ (char t m mono) p1 p2 eq ) |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
83 lemma3 : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
84 → (eq : A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] ) → m o (f← o k p1 p2 eq ) ≈ p1 |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
85 lemma3 {d} p1 p2 eq = begin |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
86 m o (f← o k p1 p2 eq ) ≈⟨ assoc ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
87 (m o f← ) o k p1 p2 eq ≈⟨ car (IsoL.iso≈L (IsTopos.ker-char (isTopos t) m mono )) ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
88 equalizer (Ker t (char t m mono)) o k p1 p2 eq ≈⟨ IsEqualizer.ek=h (isEqualizer (Ker t (char t m mono))) ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
89 p1 ∎ |
| 978 | 90 uniq : {d : Obj A} (p' : Hom A d b) (π1' : Hom A d a) (π2' : Hom A d １) |
| 91 (eq : A [ A [ char t m mono o π1' ] ≈ A [ ⊤ t o π2' ] ]) → | |
| 92 A [ A [ m o p' ] ≈ π1' ] → A [ A [ ○ b o p' ] ≈ π2' ] → f← o k π1' π2' eq ≈ p' | |
| 93 uniq {d} p p1 p2 eq pe1 pe2 = begin | |
| 979 | 94 f← o k p1 p2 eq ≈⟨ cdr ( IsEqualizer.uniqueness (isEqualizer (Ker t (char t m mono))) lemma4) ⟩ |
| 95 f← o (f→ o p ) ≈⟨ assoc ⟩ | |
| 96 (f← o f→ ) o p ≈⟨ car (Iso.iso→ (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono ))) ⟩ | |
| 97 id1 A _ o p ≈⟨ idL ⟩ | |
| 98 p ∎ where | |
| 99 lemma4 : A [ A [ equalizer (Ker t (char t m mono)) o (f→ o p) ] ≈ p1 ] | |
| 100 lemma4 = begin | |
| 101 equalizer (Ker t (char t m mono)) o (f→ o p) ≈⟨ assoc ⟩ | |
| 102 (equalizer (Ker t (char t m mono)) o f→ ) o p ≈⟨ car (IsoL.L≈iso (IsTopos.ker-char (isTopos t) m mono )) ⟩ | |
| 103 m o p ≈⟨ pe1 ⟩ | |
| 104 p1 ∎ where | |
| 978 | 105 |
| 965 | 106 |
| 971 | 107 δmono : {b : Obj A } → Mono A < id1 A b , id1 A b > |
| 108 δmono = record { | |
| 109 isMono = m1 | |
| 110 } where | |
| 111 m1 : {d b : Obj A} (f g : Hom A d b) → A [ A [ < id1 A b , id1 A b > o f ] ≈ A [ < id1 A b , id1 A b > o g ] ] → A [ f ≈ g ] | |
| 972 | 112 m1 {d} {b} f g eq = begin |
| 113 f ≈↑⟨ idL ⟩ | |
| 114 id1 A _ o f ≈↑⟨ car (IsCCC.e3a isCCC) ⟩ | |
| 115 (π o < id1 A b , id1 A b >) o f ≈↑⟨ assoc ⟩ | |
| 116 π o (< id1 A b , id1 A b > o f) ≈⟨ cdr eq ⟩ | |
| 117 π o (< id1 A b , id1 A b > o g) ≈⟨ assoc ⟩ | |
| 118 (π o < id1 A b , id1 A b >) o g ≈⟨ car (IsCCC.e3a isCCC) ⟩ | |
| 119 id1 A _ o g ≈⟨ idL ⟩ | |
| 120 g ∎ | |
| 965 | 121 |
| 971 | 122 prop32→ : {a b : Obj A}→ (f g : Hom A a b ) |
| 123 → A [ f ≈ g ] → A [ A [ char t < id1 A b , id1 A b > δmono o < f , g > ] ≈ A [ ⊤ t o ○ a ] ] | |
| 972 | 124 prop32→ {a} {b} f g f=g = begin |
| 125 char t < id1 A b , id1 A b > δmono o < f , g > ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom (sym f=g)) ⟩ | |
| 126 char t < id1 A b , id1 A b > δmono o < f , f > ≈↑⟨ cdr ( IsCCC.π-cong isCCC idL idL ) ⟩ | |
| 127 char t < id1 A b , id1 A b > δmono o < id1 A _ o f , id1 A _ o f > ≈↑⟨ cdr ( IsCCC.distr-π isCCC ) ⟩ | |
| 128 char t < id1 A b , id1 A b > δmono o (< id1 A _ , id1 A _ > o f) ≈⟨ assoc ⟩ | |
| 975 | 129 (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 ) ⟩ |
| 972 | 130 (⊤ t o ○ b) o f ≈↑⟨ assoc ⟩ |
| 131 ⊤ t o (○ b o f) ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ | |
| 975 | 132 ⊤ t o ○ a ∎ |
| 971 | 133 |
| 134 prop23→ : {a b : Obj A}→ (f g : Hom A a b ) | |
| 135 → A [ A [ char t < id1 A b , id1 A b > δmono o < f , g > ] ≈ A [ ⊤ t o ○ a ] ] → A [ f ≈ g ] | |
| 979 | 136 prop23→ {a} {b} f g eq = begin |
| 137 f ≈⟨ IsCCC.π≈ isCCC p2 ⟩ | |
| 138 k ≈↑⟨ IsCCC.π'≈ isCCC p2 ⟩ | |
| 139 g ∎ | |
| 140 where | |
| 976 | 141 δb : Hom A ( b ∧ b ) (Ω t) |
| 142 δb = char t < id1 A b , id1 A b > δmono | |
| 143 ip : Pullback A δb (⊤ t) | |
| 144 ip = topos-m-pullback < id1 A b , id1 A b > δmono | |
| 145 k : Hom A a b | |
| 146 k = IsPullback.pullback (Pullback.isPullback ip ) eq | |
| 979 | 147 p2 : < f , g > ≈ < k , k > |
| 976 | 148 p2 = begin |
| 979 | 149 < f , g > ≈↑⟨ IsPullback.π1p=π1 (Pullback.isPullback ip) ⟩ |
| 150 < id1 A b , id1 A b > o k ≈⟨ IsCCC.distr-π isCCC ⟩ | |
| 151 < id1 A b o k , id1 A b o k > ≈⟨ IsCCC.π-cong isCCC idL idL ⟩ | |
| 152 < k , k > ∎ | |
| 971 | 153 |
| 154 N : (n : ToposNat A １ ) → Obj A | |
| 155 N n = NatD.Nat (ToposNat.TNat n) | |
| 156 | |
| 972 | 157 record prop33 (n : ToposNat A １ ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where |
| 971 | 158 field |
| 972 | 159 g : {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → Hom A (N n) a |
| 160 g0=f : {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → A [ A [ g f h o NatD.nzero (ToposNat.TNat n) ] ≈ f ] | |
| 161 gs=h : {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N n ∧ a) a ) → A [ A [ g f h o NatD.nsuc (ToposNat.TNat n) ] ≈ A [ h o < id1 A _ , g f h > ] ] | |
| 162 g-cong : {a : Obj A} {f f' : Hom A １ a } { h h' : Hom A (N n ∧ a) a } → A [ f ≈ f' ] → A [ h ≈ h' ] → A [ g f h ≈ g f' h' ] | |
| 971 | 163 |
| 979 | 164 p33 : (n : ToposNat A １ ) → prop33 n |
| 165 p33 = {!!} | |
| 166 | |
| 971 | 167 cor33 : (n : ToposNat A １ ) |
| 168 → coProduct A １ ( NatD.Nat (ToposNat.TNat n) ) -- N ≅ N + 1 | |
| 979 | 169 cor33 n = record { |
| 971 | 170 coproduct = N n |
| 171 ; κ1 = NatD.nzero (ToposNat.TNat n) | |
| 972 | 172 ; κ2 = NatD.nsuc (ToposNat.TNat n) |
| 971 | 173 ; isProduct = record { |
| 972 | 174 _+_ = λ {a} f g → prop33.g p f ( g o π ) -- Hom A (N n ∧ a) a |
| 175 ; κ1f+g=f = λ {a} {f} {g} → prop33.g0=f p f (g o π ) | |
| 176 ; κ2f+g=g = k2 | |
| 971 | 177 ; uniqueness = {!!} |
| 972 | 178 ; +-cong = λ f=f' g=g' → prop33.g-cong p f=f' (resp refl-hom g=g' ) |
| 971 | 179 |
| 180 } | |
| 972 | 181 } where |
| 979 | 182 p = p33 n |
| 972 | 183 k2 : {a : Obj A} {f : Hom A １ a} {g : Hom A (NatD.Nat (ToposNat.TNat n)) a } |
| 184 → A [ A [ prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n) ] ≈ g ] | |
| 185 k2 {a} {f} {g} = begin | |
| 186 (prop33.g p f ((A Category.o g) π) o NatD.nsuc (ToposNat.TNat n)) ≈⟨ prop33.gs=h p f (g o π ) ⟩ | |
| 187 ( g o π ) o < id1 A (N n) , prop33.g p f (g o π) > ≈⟨ sym assoc ⟩ | |
| 188 g o ( π o < id1 A (N n) , prop33.g p f (g o π) >) ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩ | |
| 189 g o id1 A (N n) ≈⟨ idR ⟩ | |
| 190 g ∎ | |
| 191 | |
| 192 | |
| 193 |