Mercurial > hg > Members > kono > Proof > category
annotate src/ToposEx.agda @ 981:0e417c508096
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Mar 2021 04:51:55 +0900 |
| parents | 8ab4307d9337 |
| children | 888e6613b99a |
| 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 | |
| 980 | 6 module ToposEx {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.１ 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 |
| 980 | 154 open NatD |
| 155 open ToposNat n | |
| 971 | 156 |
| 980 | 157 N : Obj A |
| 158 N = Nat TNat | |
| 159 | |
| 160 record prop33 {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N ∧ a) a ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where | |
| 971 | 161 field |
| 980 | 162 g : Hom A N a |
| 163 g0=f : A [ A [ g o nzero TNat ] ≈ f ] | |
| 164 gs=h : A [ A [ g o nsuc TNat ] ≈ A [ h o < id1 A _ , g > ] ] | |
| 979 | 165 |
| 980 | 166 p33 : {a : Obj A} (z : Hom A １ a ) ( h : Hom A (N ∧ a) a ) → prop33 z h |
| 167 p33 {a} z h = record { | |
| 168 g = g | |
| 169 ; g0=f = iii | |
| 170 ; gs=h = v | |
| 171 } where | |
| 172 xnat : NatD A １ | |
| 173 xnat = record { Nat = N ∧ a ; nzero = < nzero TNat , z > ; nsuc = < nsuc TNat o π , h > } | |
| 174 fg : Hom A N (N ∧ a ) | |
| 175 fg = gNat xnat | |
| 176 f : Hom A N N | |
| 177 f = π o fg | |
| 178 g : Hom A N a | |
| 179 g = π' o fg | |
| 981 | 180 ig : f ≈ id1 A N |
| 181 ig = begin | |
| 182 f ≈⟨ nat-unique TNat {!!} {!!} ⟩ | |
| 183 gNat TNat ≈↑⟨ nat-unique TNat idL (trans-hom idL (sym idR) ) ⟩ | |
| 980 | 184 id1 A _ ∎ |
| 185 i : f o nzero TNat ≈ nzero TNat | |
| 186 i = begin | |
| 187 f o nzero TNat ≈⟨ car ig ⟩ id1 A _ o nzero TNat ≈⟨ idL ⟩ | |
| 188 nzero TNat ∎ | |
| 189 ii : f o nsuc TNat ≈ nsuc TNat o f | |
| 190 ii = begin | |
| 191 f o nsuc TNat ≈⟨ car ig ⟩ id1 A _ o nsuc TNat ≈⟨ idL ⟩ nsuc TNat ≈↑⟨ idR ⟩ nsuc TNat o id1 A _ ≈↑⟨ cdr ig ⟩ | |
| 192 nsuc TNat o f ∎ | |
| 193 iii : g o nzero TNat ≈ z | |
| 194 iii = begin | |
| 195 g o nzero TNat ≈⟨⟩ (π' o gNat xnat ) o nzero TNat ≈↑⟨ assoc ⟩ | |
| 196 π' o ( gNat xnat o nzero TNat) ≈⟨ cdr (IsToposNat.izero isToposN xnat) ⟩ | |
| 197 π' o < nzero TNat , z > ≈⟨ IsCCC.e3b isCCC ⟩ | |
| 198 z ∎ | |
| 199 iv : g o nsuc TNat ≈ h o < f , g > | |
| 200 iv = begin | |
| 201 g o nsuc TNat ≈⟨⟩ | |
| 202 (π' o gNat xnat) o nsuc TNat ≈↑⟨ assoc ⟩ | |
| 203 π' o (gNat xnat o nsuc TNat ) ≈⟨ cdr (IsToposNat.isuc isToposN xnat) ⟩ | |
| 204 π' o (nsuc xnat o gNat xnat ) ≈⟨ assoc ⟩ | |
| 205 (π' o nsuc xnat ) o gNat xnat ≈⟨ car (IsCCC.e3b isCCC) ⟩ | |
| 206 h o gNat xnat ≈↑⟨ cdr (IsCCC.e3c isCCC) ⟩ | |
| 207 h o < π o fg , π' o fg > ≈⟨⟩ | |
| 208 h o < f , g > ∎ | |
| 209 v : A [ A [ g o nsuc TNat ] ≈ A [ h o < id1 A N , g > ] ] | |
| 210 v = begin | |
| 211 g o nsuc TNat ≈⟨ iv ⟩ | |
| 212 h o < f , g > ≈⟨ cdr ( IsCCC.π-cong isCCC ig refl-hom) ⟩ | |
| 213 h o < id1 A N , g > ∎ | |
| 214 | |
| 215 | |
| 216 cor33 : coProduct A １ (Nat TNat ) -- N ≅ N + 1 | |
| 217 cor33 = record { | |
| 218 coproduct = N | |
| 219 ; κ1 = nzero TNat | |
| 220 ; κ2 = nsuc TNat | |
| 971 | 221 ; isProduct = record { |
| 980 | 222 _+_ = λ {a} f g → prop33.g (p f ( g o π )) -- Hom A (N n ∧ a) a |
| 223 ; κ1f+g=f = λ {a} {f} {g} → prop33.g0=f (p f (g o π ) ) | |
| 224 ; κ2f+g=g = λ {a} {f} {g} → k2 {a} {f} {g} | |
| 971 | 225 ; uniqueness = {!!} |
| 980 | 226 ; +-cong = λ f=f' g=g' → {!!} -- prop33.g-cong p f=f' (resp refl-hom g=g' ) |
| 971 | 227 } |
| 972 | 228 } where |
| 980 | 229 p : {a : Obj A} (f : Hom A １ a) ( h : Hom A (N ∧ a) a ) → prop33 f h |
| 230 p f h = p33 f h | |
| 231 k2 : {a : Obj A} {f : Hom A １ a} {g : Hom A (Nat TNat) a } | |
| 232 → A [ A [ prop33.g (p f (g o π)) o nsuc TNat ] ≈ g ] | |
| 972 | 233 k2 {a} {f} {g} = begin |
| 980 | 234 (prop33.g (p f (g o π)) o nsuc TNat) ≈⟨ prop33.gs=h (p f (g o π )) ⟩ |
| 235 ( g o π ) o < id1 A N , prop33.g (p f (g o π)) > ≈⟨ sym assoc ⟩ | |
| 236 g o ( π o < id1 A N , prop33.g (p f (g o π)) >) ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩ | |
| 237 g o id1 A N ≈⟨ idR ⟩ | |
| 972 | 238 g ∎ |
| 239 | |
| 240 | |
| 241 |