Mercurial > hg > Members > kono > Proof > category
annotate src/ToposEx.agda @ 1089:77e40cea8264
i : {b c : Obj A} (f : Hom A b c ) → ¬ ( f ≅ x ) → φ x f is bad
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 17 May 2021 00:42:08 +0900 |
| parents | 60b24b3dc0c6 |
| children | 45de2b31bf02 |
| rev | line source |
|---|---|
| 1038 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 963 | 2 open import CCC |
| 3 open import Level | |
| 4 open import Category | |
| 5 open import cat-utility | |
| 6 open import HomReasoning | |
| 980 | 7 module ToposEx {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.１ c)) where |
| 963 | 8 |
| 974 | 9 open Topos |
| 10 open Equalizer | |
| 11 open ≈-Reasoning A | |
| 12 open CCC.CCC c | |
| 13 | |
| 1038 | 14 -- |
| 963 | 15 -- ○ b |
| 16 -- b -----------→ 1 | |
| 17 -- | | | |
| 18 -- m | | ⊤ | |
| 19 -- ↓ char m ↓ | |
| 20 -- a -----------→ Ω | |
| 21 -- h | |
| 964 | 22 -- |
| 23 -- Ker t h : Equalizer A h (A [ ⊤ o (○ a) ]) | |
| 963 | 24 |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
25 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
|
26 → 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
|
27 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
|
28 h o p1 ≈⟨ eq ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
29 ⊤ t o p2 ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
30 ⊤ t o (○ d) ≈↑⟨ cdr (IsCCC.e2 isCCC) ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
31 ⊤ t o ( ○ a o p1 ) ≈⟨ assoc ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
32 (⊤ t o ○ a ) o p1 ∎ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
33 |
| 986 | 34 ---- |
| 35 -- | |
| 36 -- pull back from h | |
| 37 -- | |
| 974 | 38 topos-pullback : {a : Obj A} → (h : Hom A a (Ω t)) → Pullback A h (⊤ t) |
| 39 topos-pullback {a} h = record { | |
| 963 | 40 ab = equalizer-c (Ker t h) -- b |
| 41 ; π1 = equalizer (Ker t h) -- m | |
| 42 ; π2 = ○ ( equalizer-c (Ker t h) ) -- ○ b | |
| 43 ; isPullback = record { | |
| 44 commute = comm | |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
45 ; pullback = λ {d} {p1} {p2} eq → IsEqualizer.k (isEqualizer (Ker t h)) p1 (mh=⊤ h p1 p2 eq ) |
| 964 | 46 ; π1p=π1 = IsEqualizer.ek=h (isEqualizer (Ker t h)) |
| 47 ; π2p=π2 = λ {d} {p1'} {p2'} {eq} → lemma2 eq | |
| 48 ; uniqueness = uniq | |
| 963 | 49 } |
| 974 | 50 } where |
| 51 e2 = IsCCC.e2 isCCC | |
| 963 | 52 comm : A [ A [ h o equalizer (Ker t h) ] ≈ A [ ⊤ t o ○ (equalizer-c (Ker t h)) ] ] |
| 53 comm = begin | |
| 964 | 54 h o equalizer (Ker t h) ≈⟨ IsEqualizer.fe=ge (isEqualizer (Ker t h)) ⟩ |
| 55 (⊤ t o ○ a ) o equalizer (Ker t h) ≈↑⟨ assoc ⟩ | |
| 974 | 56 ⊤ t o (○ a o equalizer (Ker t h)) ≈⟨ cdr e2 ⟩ |
| 963 | 57 ⊤ t o ○ (equalizer-c (Ker t h)) ∎ |
| 964 | 58 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
|
59 → A [ A [ ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(mh=⊤ h p1' p2' eq) ] ≈ p2' ] |
| 964 | 60 lemma2 {d} {p1'} {p2'} eq = begin |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
61 ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(mh=⊤ h p1' p2' eq) ≈⟨ e2 ⟩ |
| 964 | 62 ○ d ≈↑⟨ e2 ⟩ |
| 63 p2' ∎ | |
| 976 | 64 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' ] ]) |
| 65 (π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
|
66 → A [ IsEqualizer.k (isEqualizer (Ker t h)) π1' (mh=⊤ h π1' π2' eq) ≈ p' ] |
| 976 | 67 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
|
68 IsEqualizer.k (isEqualizer (Ker t h)) p1' (mh=⊤ h p1' p2' eq) ≈⟨ IsEqualizer.uniqueness (isEqualizer (Ker t h)) pe1 ⟩ |
| 964 | 69 p' ∎ |
| 963 | 70 |
| 986 | 71 ---- |
| 72 -- | |
| 73 -- pull back from m | |
| 74 -- | |
| 974 | 75 topos-m-pullback : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono ) (⊤ t) |
| 976 | 76 topos-m-pullback {a} {b} m mono = record { |
| 77 ab = b | |
| 78 ; π1 = m | |
| 79 ; π2 = ○ b | |
| 80 ; isPullback = record { | |
|
1017
90224a662c4e
two equalizers in Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1016
diff
changeset
|
81 commute = IsTopos.char-m=⊤ (Topos.isTopos t) m mono |
| 1018 | 82 ; pullback = λ {d} {p1} {p2} eq → k p1 p2 eq |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
83 ; π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
|
84 ; π2p=π2 = λ {d} {p1'} {p2'} {eq} → trans-hom (IsCCC.e2 isCCC) (sym (IsCCC.e2 isCCC)) |
| 979 | 85 ; uniqueness = uniq |
| 976 | 86 } |
| 87 } where | |
| 1018 | 88 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 b |
| 89 k p1 p2 eq = IsEqualizer.k (IsTopos.ker-m (isTopos t) m mono) p1 (mh=⊤ (char t m mono) p1 p2 eq ) | |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
90 lemma3 : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) |
| 1018 | 91 → (eq : A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] ) → m o (k p1 p2 eq ) ≈ p1 |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
92 lemma3 {d} p1 p2 eq = begin |
| 1018 | 93 m o k p1 p2 eq ≈⟨ IsEqualizer.ek=h (IsTopos.ker-m (isTopos t) m mono) ⟩ |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
94 p1 ∎ |
| 978 | 95 uniq : {d : Obj A} (p' : Hom A d b) (π1' : Hom A d a) (π2' : Hom A d １) |
| 96 (eq : A [ A [ char t m mono o π1' ] ≈ A [ ⊤ t o π2' ] ]) → | |
| 1018 | 97 A [ A [ m o p' ] ≈ π1' ] → A [ A [ ○ b o p' ] ≈ π2' ] → k π1' π2' eq ≈ p' |
| 978 | 98 uniq {d} p p1 p2 eq pe1 pe2 = begin |
| 1018 | 99 k p1 p2 eq ≈⟨ IsEqualizer.uniqueness (IsTopos.ker-m (isTopos t) m mono) pe1 ⟩ |
| 100 p ∎ | |
| 965 | 101 |
| 971 | 102 δmono : {b : Obj A } → Mono A < id1 A b , id1 A b > |
| 103 δmono = record { | |
| 104 isMono = m1 | |
| 105 } where | |
| 106 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 | 107 m1 {d} {b} f g eq = begin |
| 108 f ≈↑⟨ idL ⟩ | |
| 109 id1 A _ o f ≈↑⟨ car (IsCCC.e3a isCCC) ⟩ | |
| 110 (π o < id1 A b , id1 A b >) o f ≈↑⟨ assoc ⟩ | |
| 111 π o (< id1 A b , id1 A b > o f) ≈⟨ cdr eq ⟩ | |
| 112 π o (< id1 A b , id1 A b > o g) ≈⟨ assoc ⟩ | |
| 113 (π o < id1 A b , id1 A b >) o g ≈⟨ car (IsCCC.e3a isCCC) ⟩ | |
| 114 id1 A _ o g ≈⟨ idL ⟩ | |
| 115 g ∎ | |
| 965 | 116 |
| 984 | 117 -- |
| 986 | 118 -- |
| 1035 | 119 -- Hom equality and Ω (p.94 cl(Δ a) in Takeuchi ) |
| 986 | 120 -- |
| 121 -- | |
| 984 | 122 -- a -----------→ + |
| 123 -- f||g ○ a | | |
| 124 -- ↓↓ | | |
| 125 -- b -----------→ 1 | |
| 126 -- | ○ b | | |
| 127 -- <1,1> | | ⊤ | |
| 128 -- ↓ ↓ | |
| 129 -- b ∧ b ---------→ Ω | |
| 130 -- char <1,1> | |
| 131 | |
| 971 | 132 prop32→ : {a b : Obj A}→ (f g : Hom A a b ) |
| 133 → A [ f ≈ g ] → A [ A [ char t < id1 A b , id1 A b > δmono o < f , g > ] ≈ A [ ⊤ t o ○ a ] ] | |
| 972 | 134 prop32→ {a} {b} f g f=g = begin |
| 135 char t < id1 A b , id1 A b > δmono o < f , g > ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom (sym f=g)) ⟩ | |
| 136 char t < id1 A b , id1 A b > δmono o < f , f > ≈↑⟨ cdr ( IsCCC.π-cong isCCC idL idL ) ⟩ | |
| 137 char t < id1 A b , id1 A b > δmono o < id1 A _ o f , id1 A _ o f > ≈↑⟨ cdr ( IsCCC.distr-π isCCC ) ⟩ | |
| 138 char t < id1 A b , id1 A b > δmono o (< id1 A _ , id1 A _ > o f) ≈⟨ assoc ⟩ | |
|
1017
90224a662c4e
two equalizers in Topos
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1016
diff
changeset
|
139 (char t < id1 A b , id1 A b > δmono o < id1 A b , id1 A b > ) o f ≈⟨ car (IsTopos.char-m=⊤ (Topos.isTopos t) _ δmono ) ⟩ |
| 972 | 140 (⊤ t o ○ b) o f ≈↑⟨ assoc ⟩ |
| 141 ⊤ t o (○ b o f) ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ | |
| 975 | 142 ⊤ t o ○ a ∎ |
| 971 | 143 |
| 144 prop23→ : {a b : Obj A}→ (f g : Hom A a b ) | |
| 145 → A [ A [ char t < id1 A b , id1 A b > δmono o < f , g > ] ≈ A [ ⊤ t o ○ a ] ] → A [ f ≈ g ] | |
| 979 | 146 prop23→ {a} {b} f g eq = begin |
| 147 f ≈⟨ IsCCC.π≈ isCCC p2 ⟩ | |
| 148 k ≈↑⟨ IsCCC.π'≈ isCCC p2 ⟩ | |
| 149 g ∎ | |
| 150 where | |
| 976 | 151 δb : Hom A ( b ∧ b ) (Ω t) |
| 152 δb = char t < id1 A b , id1 A b > δmono | |
| 153 ip : Pullback A δb (⊤ t) | |
| 154 ip = topos-m-pullback < id1 A b , id1 A b > δmono | |
| 155 k : Hom A a b | |
| 156 k = IsPullback.pullback (Pullback.isPullback ip ) eq | |
| 979 | 157 p2 : < f , g > ≈ < k , k > |
| 976 | 158 p2 = begin |
| 979 | 159 < f , g > ≈↑⟨ IsPullback.π1p=π1 (Pullback.isPullback ip) ⟩ |
| 160 < id1 A b , id1 A b > o k ≈⟨ IsCCC.distr-π isCCC ⟩ | |
| 161 < id1 A b o k , id1 A b o k > ≈⟨ IsCCC.π-cong isCCC idL idL ⟩ | |
| 162 < k , k > ∎ | |
| 986 | 163 -- |
| 164 -- | |
| 165 -- Initial Natural number diagram | |
| 166 -- | |
| 167 -- | |
| 971 | 168 |
| 980 | 169 open NatD |
| 170 open ToposNat n | |
| 971 | 171 |
| 984 | 172 -- 0 suc |
| 173 -- 1 -----------→ N ---------→ N | |
| 174 -- | | | | |
| 175 -- | <f,g> | <f,g>| | |
| 176 -- | ↓ ↓ | |
| 177 -- 1 ---------→ N x A -----→ N x A | |
| 178 -- <0,z> <suc o π , h > | |
| 179 | |
| 980 | 180 N : Obj A |
| 986 | 181 N = Nat iNat |
| 1034 | 182 -- if h : Hom A (N ∧ a) a is π', A is a constant |
| 980 | 183 |
| 184 record prop33 {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N ∧ a) a ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where | |
| 971 | 185 field |
| 980 | 186 g : Hom A N a |
| 986 | 187 g0=f : A [ A [ g o nzero iNat ] ≈ f ] |
| 188 gs=h : A [ A [ g o nsuc iNat ] ≈ A [ h o < id1 A _ , g > ] ] | |
| 982 | 189 xnat : NatD A １ |
| 979 | 190 |
| 980 | 191 p33 : {a : Obj A} (z : Hom A １ a ) ( h : Hom A (N ∧ a) a ) → prop33 z h |
| 192 p33 {a} z h = record { | |
| 193 g = g | |
| 194 ; g0=f = iii | |
| 195 ; gs=h = v | |
| 982 | 196 ; xnat = xnat |
| 980 | 197 } where |
| 198 xnat : NatD A １ | |
| 986 | 199 xnat = record { Nat = N ∧ a ; nzero = < nzero iNat , z > ; nsuc = < nsuc iNat o π , h > } |
| 980 | 200 fg : Hom A N (N ∧ a ) |
| 986 | 201 fg = initialNat xnat -- < f , g > |
| 980 | 202 f : Hom A N N |
| 203 f = π o fg | |
| 204 g : Hom A N a | |
| 205 g = π' o fg | |
| 986 | 206 i : f o nzero iNat ≈ nzero iNat |
| 980 | 207 i = begin |
| 986 | 208 f o nzero iNat ≈⟨⟩ |
| 209 (π o fg) o nzero iNat ≈↑⟨ assoc ⟩ | |
| 210 π o (fg o nzero iNat ) ≈⟨ cdr (IsToposNat.izero isToposN xnat ) ⟩ | |
| 982 | 211 π o nzero xnat ≈⟨ IsCCC.e3a isCCC ⟩ |
| 986 | 212 nzero iNat ∎ |
| 213 ii : f o nsuc iNat ≈ nsuc iNat o f | |
| 980 | 214 ii = begin |
| 986 | 215 f o nsuc iNat ≈⟨⟩ |
| 216 (π o fg ) o nsuc iNat ≈↑⟨ assoc ⟩ | |
| 217 π o ( fg o nsuc iNat ) ≈⟨ cdr (IsToposNat.isuc isToposN xnat ) ⟩ | |
| 218 π o (nsuc xnat o initialNat xnat) ≈⟨ assoc ⟩ | |
| 219 (π o < nsuc iNat o π , h > ) o initialNat xnat ≈⟨ car (IsCCC.e3a isCCC) ⟩ | |
| 220 ( nsuc iNat o π ) o initialNat xnat ≈↑⟨ assoc ⟩ | |
| 221 nsuc iNat o ( π o initialNat xnat ) ≈⟨⟩ | |
| 222 nsuc iNat o f ∎ | |
| 982 | 223 ig : f ≈ id1 A N |
| 224 ig = begin | |
| 986 | 225 f ≈⟨ nat-unique iNat i ii ⟩ |
| 226 initialNat iNat ≈↑⟨ nat-unique iNat idL (trans-hom idL (sym idR) ) ⟩ | |
| 982 | 227 id1 A _ ∎ |
| 986 | 228 iii : g o nzero iNat ≈ z |
| 980 | 229 iii = begin |
| 986 | 230 g o nzero iNat ≈⟨⟩ (π' o initialNat xnat ) o nzero iNat ≈↑⟨ assoc ⟩ |
| 231 π' o ( initialNat xnat o nzero iNat) ≈⟨ cdr (IsToposNat.izero isToposN xnat) ⟩ | |
| 232 π' o < nzero iNat , z > ≈⟨ IsCCC.e3b isCCC ⟩ | |
| 980 | 233 z ∎ |
| 986 | 234 iv : g o nsuc iNat ≈ h o < f , g > |
| 980 | 235 iv = begin |
| 986 | 236 g o nsuc iNat ≈⟨⟩ |
| 237 (π' o initialNat xnat) o nsuc iNat ≈↑⟨ assoc ⟩ | |
| 238 π' o (initialNat xnat o nsuc iNat ) ≈⟨ cdr (IsToposNat.isuc isToposN xnat) ⟩ | |
| 239 π' o (nsuc xnat o initialNat xnat ) ≈⟨ assoc ⟩ | |
| 240 (π' o nsuc xnat ) o initialNat xnat ≈⟨ car (IsCCC.e3b isCCC) ⟩ | |
| 241 h o initialNat xnat ≈↑⟨ cdr (IsCCC.e3c isCCC) ⟩ | |
| 980 | 242 h o < π o fg , π' o fg > ≈⟨⟩ |
| 243 h o < f , g > ∎ | |
| 986 | 244 v : A [ A [ g o nsuc iNat ] ≈ A [ h o < id1 A N , g > ] ] |
| 980 | 245 v = begin |
| 986 | 246 g o nsuc iNat ≈⟨ iv ⟩ |
| 980 | 247 h o < f , g > ≈⟨ cdr ( IsCCC.π-cong isCCC ig refl-hom) ⟩ |
| 248 h o < id1 A N , g > ∎ | |
| 249 | |
| 984 | 250 -- . |
| 251 -- / | \ | |
| 252 -- / | \ | |
| 253 -- / ↓ \ | |
| 254 -- N --→ N ←-- a | |
| 255 -- | |
| 986 | 256 cor33 : coProduct A １ (Nat iNat ) -- N ≅ N + 1 |
| 980 | 257 cor33 = record { |
| 258 coproduct = N | |
| 986 | 259 ; κ1 = nzero iNat |
| 260 ; κ2 = nsuc iNat | |
| 971 | 261 ; isProduct = record { |
| 980 | 262 _+_ = λ {a} f g → prop33.g (p f ( g o π )) -- Hom A (N n ∧ a) a |
| 263 ; κ1f+g=f = λ {a} {f} {g} → prop33.g0=f (p f (g o π ) ) | |
| 264 ; κ2f+g=g = λ {a} {f} {g} → k2 {a} {f} {g} | |
| 982 | 265 ; uniqueness = uniq |
| 983 | 266 ; +-cong = pcong |
| 971 | 267 } |
| 972 | 268 } where |
| 980 | 269 p : {a : Obj A} (f : Hom A １ a) ( h : Hom A (N ∧ a) a ) → prop33 f h |
| 270 p f h = p33 f h | |
| 986 | 271 k2 : {a : Obj A} {f : Hom A １ a} {g : Hom A (Nat iNat) a } |
| 272 → A [ A [ prop33.g (p f (g o π)) o nsuc iNat ] ≈ g ] | |
| 972 | 273 k2 {a} {f} {g} = begin |
| 986 | 274 (prop33.g (p f (g o π)) o nsuc iNat) ≈⟨ prop33.gs=h (p f (g o π )) ⟩ |
| 980 | 275 ( g o π ) o < id1 A N , prop33.g (p f (g o π)) > ≈⟨ sym assoc ⟩ |
| 276 g o ( π o < id1 A N , prop33.g (p f (g o π)) >) ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩ | |
| 277 g o id1 A N ≈⟨ idR ⟩ | |
| 972 | 278 g ∎ |
| 986 | 279 pp : {c : Obj A} {h : Hom A (Nat iNat) c} → prop33 ( h o nzero iNat ) ( (h o nsuc iNat) o π) |
| 280 pp {c} {h} = p ( h o nzero iNat ) ( (h o nsuc iNat) o π) | |
| 281 uniq : {c : Obj A} {h : Hom A (Nat iNat) c} → | |
| 982 | 282 prop33.g pp ≈ h |
| 283 uniq {c} {h} = begin | |
| 983 | 284 prop33.g pp ≈⟨⟩ |
| 986 | 285 π' o initialNat (prop33.xnat pp) ≈↑⟨ cdr (nat-unique (prop33.xnat pp) ( |
| 983 | 286 begin |
| 986 | 287 < id1 A _ , h > o nzero iNat ≈⟨ IsCCC.distr-π isCCC ⟩ |
| 288 < id1 A _ o nzero iNat , h o nzero iNat > ≈⟨ IsCCC.π-cong isCCC idL refl-hom ⟩ | |
| 289 < nzero iNat , h o nzero iNat > ≈⟨⟩ | |
| 983 | 290 nzero (prop33.xnat pp) ∎ ) |
| 291 (begin | |
| 986 | 292 < id1 A _ , h > o nsuc iNat ≈⟨ IsCCC.distr-π isCCC ⟩ |
| 293 < id1 A _ o nsuc iNat , h o nsuc iNat > ≈⟨ IsCCC.π-cong isCCC idL refl-hom ⟩ | |
| 294 < nsuc iNat , h o nsuc iNat > ≈↑⟨ IsCCC.π-cong isCCC idR idR ⟩ | |
| 295 < nsuc iNat o id1 A _ , (h o nsuc iNat ) o id1 A _ > ≈↑⟨ IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC)) (cdr (IsCCC.e3a isCCC)) ⟩ | |
| 296 < nsuc iNat o ( π o < id1 A _ , h > ) , (h o nsuc iNat ) o ( π o < id1 A _ , h > ) > ≈⟨ IsCCC.π-cong isCCC assoc assoc ⟩ | |
| 297 < (nsuc iNat o π ) o < id1 A _ , h > , ((h o nsuc iNat ) o π ) o < id1 A _ , h > > ≈↑⟨ IsCCC.distr-π isCCC ⟩ | |
| 298 < nsuc iNat o π , (h o nsuc iNat ) o π > o < id1 A _ , h > ≈⟨⟩ | |
| 983 | 299 nsuc (prop33.xnat pp) o < id1 A _ , h > ∎ )) ⟩ |
| 300 π' o < id1 A _ , h > ≈⟨ IsCCC.e3b isCCC ⟩ | |
| 982 | 301 h ∎ |
| 986 | 302 pcong : {a : Obj A } {f f' : Hom A １ a } {g g' : Hom A (Nat iNat) a } → (f=f' : f ≈ f' ) → ( g=g' : g ≈ g' ) |
| 983 | 303 → prop33.g (p f (g o π)) ≈ prop33.g (p f' (g' o π)) |
| 304 pcong {a} {f} {f'} {g} {g'} f=f' g=g' = begin | |
| 305 prop33.g (p f (g o π)) ≈⟨⟩ | |
| 986 | 306 π' o (initialNat (prop33.xnat (p f (g o π)))) ≈↑⟨ cdr (nat-unique (prop33.xnat (p f (g o π))) lem1 lem2 ) ⟩ |
| 307 π' o (initialNat (prop33.xnat (p f' (g' o π)))) ≈⟨⟩ | |
| 983 | 308 prop33.g (p f' (g' o π)) ∎ where |
| 986 | 309 lem1 : A [ A [ initialNat (prop33.xnat (p f' ((A Category.o g') π))) o nzero iNat ] ≈ nzero (prop33.xnat (p f ((A Category.o g) π))) ] |
| 983 | 310 lem1 = begin |
| 986 | 311 initialNat (prop33.xnat (p f' (g' o π))) o nzero iNat ≈⟨ IsToposNat.izero isToposN _ ⟩ |
| 983 | 312 nzero (prop33.xnat (p f' (g' o π))) ≈⟨⟩ |
| 986 | 313 < nzero iNat , f' > ≈⟨ IsCCC.π-cong isCCC refl-hom (sym f=f') ⟩ |
| 314 < nzero iNat , f > ≈⟨⟩ | |
| 983 | 315 nzero (prop33.xnat (p f (g o π))) ∎ |
| 986 | 316 lem2 : A [ A [ initialNat (prop33.xnat (p f' (g' o π))) o nsuc iNat ] ≈ A [ nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ] ] |
| 983 | 317 lem2 = begin |
| 986 | 318 initialNat (prop33.xnat (p f' (g' o π))) o nsuc iNat ≈⟨ IsToposNat.isuc isToposN _ ⟩ |
| 319 nsuc (prop33.xnat (p f' (g' o π))) o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ | |
| 320 < (nsuc iNat) o π , g' o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨ car ( IsCCC.π-cong isCCC refl-hom (car (sym g=g')) ) ⟩ | |
| 321 < (nsuc iNat) o π , g o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ | |
| 322 nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ∎ | |
| 1035 | 323 |
| 1036 | 324 open Functor |
| 1037 | 325 open import Category.Sets hiding (_o_) |
| 1036 | 326 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym) |
| 327 | |
| 1037 | 328 record Singleton (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where |
| 329 field | |
| 330 singleton : Hom A (a ∧ a) ( CCC._<=_ c (Ω t) (a ∧ a) ) | |
| 331 scommute : A [ A [ CCC.ε c o < singleton , id1 A _ > ] ≈ char t < id1 A _ , id1 A _ > δmono ] | |
| 332 | |
| 333 tequalizer : {a b : Obj A} → (f g : Hom A a b ) → Equalizer A f g | |
| 334 tequalizer {a} {b} f g = record { | |
| 335 equalizer-c = equalizer-c ker | |
| 336 ; equalizer = equalizer ker | |
| 337 ; isEqualizer = record { | |
| 338 fe=ge = {!!} | |
| 339 ; k = {!!} | |
| 340 ; ek=h = {!!} | |
| 341 ; uniqueness = {!!} | |
| 342 } | |
| 343 } where | |
| 344 ker : Equalizer A ( A [ char t < id1 A _ , id1 A b > δmono o < f , g > ] ) (A [ ⊤ t o (CCC.○ c a) ]) | |
| 345 ker = Ker t ( A [ char t < id1 A _ , id1 A b > δmono o < f , g > ] ) | |
| 346 | |
| 347 singleton→mono : {a : Obj A} (s : Singleton a ) → Mono A (Singleton.singleton s) | |
| 348 singleton→mono {a} s = record { isMono = λ {b} f g eq → {!!} } | |
| 349 | |
| 350 record Partialmap (a b : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where | |
| 351 field | |
| 352 p : Obj A | |
| 353 d : Hom A p a | |
| 354 f : Hom A p b | |
| 355 dm : Mono A d | |
| 356 | |
| 357 record PartialmapClassifier (b : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where | |
| 358 field | |
| 359 b1 : Obj A | |
| 360 η : Hom A b b1 | |
| 361 pm : Partialmap b1 b | |
| 362 pmc : {a : Obj A} ( d f : Hom A a b) → Mono A d → Hom A a b1 | |
| 363 pb : {a : Obj A} ( d f : Hom A a b) → (dm : Mono A d ) → Pullback A (pmc d f dm) η | |
| 364 uniq : {a : Obj A} ( d f : Hom A a b) → (dm : Mono A d ) → (p : Hom A a b1) → Pullback A p η → A [ pmc d f dm ≈ p ] | |
| 365 | |
| 366 partialmapClassifier : (b : Obj A) → PartialmapClassifier b | |
| 367 partialmapClassifier = {!!} | |
| 368 | |
| 1046 | 369 record SubObject (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where |
| 370 field | |
| 371 sb : Obj A | |
| 372 sm : Hom A sb a | |
| 373 smono : Mono A sm | |
| 374 | |
| 375 record SubObjectClassifier (b : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ) where | |
| 376 field | |
| 377 sm : SubObject b | |
| 378 smc : {a : Obj A} ( d f : Hom A a b) → Mono A d → Hom A a b | |
| 379 pb : {a : Obj A} ( d f : Hom A a b) → (dm : Mono A d ) → Pullback A (smc d f dm) (id1 A _) | |
| 380 uniq : {a : Obj A} ( d f : Hom A a b) → (dm : Mono A d ) → (p : Hom A a b) → Pullback A p (id1 A _) → A [ smc d f dm ≈ p ] | |
| 381 | |
| 1037 | 382 postulate |
| 383 I : Set c₁ | |
| 384 small : Small A I | |
| 1036 | 385 |
| 1037 | 386 open import yoneda A I small |
| 1036 | 387 |
| 1037 | 388 cs : CCC SetsAop |
| 389 cs = {!!} | |
| 390 | |
| 391 toposS : Topos SetsAop cs | |
| 392 toposS = {!!} | |
| 1036 | 393 |