Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 191:9eb6a8691f02
choice function cannot jump between ordinal level
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 28 Jul 2019 14:07:08 +0900 |
parents | 6e778b0a7202 |
children | 38ecc75d93ce |
comparison
equal
deleted
inserted
replaced
190:6e778b0a7202 | 191:9eb6a8691f02 |
---|---|
236 in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } | 236 in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } |
237 | 237 |
238 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) | 238 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) |
239 | 239 |
240 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n} | 240 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n} |
241 ZFSubset A x = record { def = λ y → def A y ∧ def x y } where | 241 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set |
242 | 242 |
243 Def : {n : Level} → (A : OD {suc n}) → OD {suc n} | 243 Def : {n : Level} → (A : OD {suc n}) → OD {suc n} |
244 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) -- Ord x does not help ord-power→ | 244 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) |
245 | 245 |
246 | 246 |
247 _⊆_ : {n : Level} ( A B : OD {suc n} ) → ∀{ x : OD {suc n} } → Set (suc n) | 247 _⊆_ : {n : Level} ( A B : OD {suc n} ) → ∀{ x : OD {suc n} } → Set (suc n) |
248 _⊆_ A B {x} = A ∋ x → B ∋ x | 248 _⊆_ A B {x} = A ∋ x → B ∋ x |
249 | 249 |
253 subset-lemma {n} {A} {x} {y} = record { | 253 subset-lemma {n} {A} {x} {y} = record { |
254 proj1 = λ z lt → proj1 (z lt) | 254 proj1 = λ z lt → proj1 (z lt) |
255 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } | 255 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } |
256 } | 256 } |
257 | 257 |
258 Def=A→Set : {n : Level} → (A : Ordinal {suc n}) → Def (Ord A) == record { def = λ x → x o< A → Set n } | |
259 Def=A→Set {n} A = record { | |
260 eq→ = λ {y} DAx y<A → {!!} | |
261 ; eq← = {!!} -- λ {y} f → {!!} | |
262 } where | |
263 | 258 |
264 -- Constructible Set on α | 259 -- Constructible Set on α |
265 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x } | 260 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x } |
266 -- L (Φ 0) = Φ | 261 -- L (Φ 0) = Φ |
267 -- L (OSuc lv n) = { Def ( L n ) } | 262 -- L (OSuc lv n) = { Def ( L n ) } |
503 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD | 498 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD |
504 choice-func X {x} not X∋x = minimul x not | 499 choice-func X {x} not X∋x = minimul x not |
505 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A | 500 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A |
506 choice X {A} X∋A not = x∋minimul A not | 501 choice X {A} X∋A not = x∋minimul A not |
507 | 502 |
508 -- choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → OD {suc n} | 503 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → OD {suc n} |
504 choice-func' X ∋-p not = lemma (lv (od→ord X )) (ord (od→ord X)) where | |
505 lemma : (lx : Nat ) ( ox : OrdinalD lx ) → OD {suc n} | |
506 lemma lx ox with ∋-p X (ord→od record { lv = lx ; ord = ox }) | |
507 lemma lx ox | yes p = (ord→od record { lv = lx ; ord = ox }) | |
508 lemma Zero (Φ 0) | no ¬p = od∅ | |
509 lemma Zero (OSuc 0 ox) | no ¬p = lemma Zero ox | |
510 lemma (Suc lx) (Φ (Suc lx)) | no ¬p = {!!} | |
511 lemma (Suc lx) (OSuc (Suc lx) ox) | no ¬p = lemma ( Suc lx ) ox | |
512 | |
509 -- | 513 -- |
510 -- another form of regularity | 514 -- another form of regularity |
511 -- | 515 -- |
512 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} | 516 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} |
513 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) | 517 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) |