Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal.agda @ 276:6f10c47e4e7a
separate choice
fix sup-o
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 09 May 2020 09:02:52 +0900 |
| parents | 2169d948159b |
| children | fbabb20f222e |
comparison
equal
deleted
inserted
replaced
| 275:455792eaa611 | 276:6f10c47e4e7a |
|---|---|
| 231 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev | 231 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev |
| 232 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → | 232 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → |
| 233 ψ (record { lv = lx ; ord = OSuc lx x₁ }) | 233 ψ (record { lv = lx ; ord = OSuc lx x₁ }) |
| 234 caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev | 234 caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev |
| 235 | 235 |
| 236 module C-Ordinal-with-choice {n : Level} where | |
| 237 | |
| 238 import OD | |
| 239 -- open inOrdinal C-Ordinal | |
| 240 open OD (C-Ordinal {n}) | |
| 241 open OD.OD | |
| 242 open _⊆_ | |
| 243 | |
| 244 o<→c< : {x y : Ordinal } → x o< y → Ord x ⊆ Ord y | |
| 245 o<→c< lt = record { incl = λ lt1 → ordtrans lt1 lt } | |
| 246 | |
| 247 ⊆→o< : {x y : Ordinal } → Ord x ⊆ Ord y → x o< osuc y | |
| 248 ⊆→o< {x} {y} lt with trio< x y | |
| 249 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc | |
| 250 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc | |
| 251 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with incl lt (o<-subst c (sym diso) refl ) | |
| 252 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) | |
| 253 | |
| 254 -- ZFSubset : (A x : OD ) → OD | |
| 255 -- ZFSubset A x = record { def = λ y → def A y ∧ def x y } | |
| 256 | |
| 257 -- Def : (A : OD ) → OD | |
| 258 -- Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) | |
| 259 | |
| 260 Ord-lemma : (a : Ordinal) → ord→od a ⊆ Ord a | |
| 261 Ord-lemma a = record { incl = λ lt → o<-subst (c<→o< lt ) refl diso } | |
| 262 | |
| 263 ⊆-trans : {a b c x : OD} → a ⊆ b → b ⊆ c → a ⊆ c | |
| 264 ⊆-trans a⊆b b⊆c = record { incl = λ a∋x → incl b⊆c (incl a⊆b a∋x) } | |
| 265 | |
| 266 _∩_ = IsZF._∩_ isZF | |
| 267 | |
| 268 -- | |
| 269 -- ord-power-lemma : {a : Ordinal} → Power (Ord a) == Def (Ord a) | |
| 270 -- ord-power-lemma {a} = record { eq→ = left ; eq← = right } where | |
| 271 -- left : {x : Ordinal} → def (Power (Ord a)) x → def (Def (Ord a)) x | |
| 272 -- left {x} lt = lemma1 where | |
| 273 -- lemma : od→ord ((Ord a) ∩ (ord→od x)) o< sup-o ( λ y → od→ord ((Ord a) ∩ (ord→od y))) | |
| 274 -- lemma = sup-o< { λ y → od→ord ((Ord a) ∩ (ord→od y))} {x} | |
| 275 -- lemma1 : x o< sup-o ( λ x → od→ord ( ZFSubset (Ord a) (ord→od x ))) | |
| 276 -- lemma1 = {!!} | |
| 277 -- right : {x : Ordinal } → def (Def (Ord a)) x → def (Power (Ord a)) x | |
| 278 -- right {x} lt = def-subst {_} {_} {Power (Ord a)} {x} (IsZF.power← isZF (Ord a) (ord→od x) {!!}) refl diso | |
| 279 -- | |
| 280 -- uncountable : (a y : Ordinal) → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y) | |
| 281 -- uncountable a y = ⊆→o< lemma where | |
| 282 -- lemma-a : (x : OD ) → _⊆_ (ZFSubset (Ord a) (ord→od y)) (Ord a) {x} | |
| 283 -- lemma-a x lt = proj1 lt | |
| 284 -- lemma : (x : OD ) → _⊆_ (Ord ( od→ord (ZFSubset (Ord a) (ord→od y)))) (Ord a) {x} | |
| 285 -- lemma x = {!!} | |
| 286 -- | |
| 287 -- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} | |
| 288 -- continuum-hyphotheis a x = lemma2 where | |
| 289 -- lemma1 : sup-o (λ x₁ → od→ord (ZFSubset (Ord a) (ord→od x₁))) o< osuc a | |
| 290 -- lemma1 = {!!} | |
| 291 -- lemma : _⊆_ (Def (Ord a)) (Ord (osuc a)) {x} | |
| 292 -- lemma = o<→c< lemma1 | |
| 293 -- lemma2 : _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} | |
| 294 -- lemma2 = subst ( λ k → _⊆_ k (Ord (osuc a)) {x} ) (sym (==→o≡ ord-power-lemma)) lemma |