Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff 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 |
line wrap: on
line diff
--- a/OD.agda Fri Jul 26 21:08:06 2019 +0900 +++ b/OD.agda Sun Jul 28 14:07:08 2019 +0900 @@ -238,10 +238,10 @@ -- Power Set of X ( or constructible by λ y → def X (od→ord y ) ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n} -ZFSubset A x = record { def = λ y → def A y ∧ def x y } where +ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set Def : {n : Level} → (A : OD {suc n}) → OD {suc n} -Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) -- Ord x does not help ord-power→ +Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) _⊆_ : {n : Level} ( A B : OD {suc n} ) → ∀{ x : OD {suc n} } → Set (suc n) @@ -255,11 +255,6 @@ ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } } -Def=A→Set : {n : Level} → (A : Ordinal {suc n}) → Def (Ord A) == record { def = λ x → x o< A → Set n } -Def=A→Set {n} A = record { - eq→ = λ {y} DAx y<A → {!!} - ; eq← = {!!} -- λ {y} f → {!!} - } where -- Constructible Set on α -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x } @@ -505,7 +500,16 @@ choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A choice X {A} X∋A not = x∋minimul A not - -- choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → OD {suc n} + choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → OD {suc n} + choice-func' X ∋-p not = lemma (lv (od→ord X )) (ord (od→ord X)) where + lemma : (lx : Nat ) ( ox : OrdinalD lx ) → OD {suc n} + lemma lx ox with ∋-p X (ord→od record { lv = lx ; ord = ox }) + lemma lx ox | yes p = (ord→od record { lv = lx ; ord = ox }) + lemma Zero (Φ 0) | no ¬p = od∅ + lemma Zero (OSuc 0 ox) | no ¬p = lemma Zero ox + lemma (Suc lx) (Φ (Suc lx)) | no ¬p = {!!} + lemma (Suc lx) (OSuc (Suc lx) ox) | no ¬p = lemma ( Suc lx ) ox + -- -- another form of regularity --