Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff HOD.agda @ 165:d16b8bf29f4f
minor fix
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 16 Jul 2019 09:57:01 +0900 |
parents | b06f5d2f34b1 |
children | ea0e7927637a |
line wrap: on
line diff
--- a/HOD.agda Mon Jul 15 19:10:08 2019 +0900 +++ b/HOD.agda Tue Jul 16 09:57:01 2019 +0900 @@ -69,8 +69,8 @@ sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ -- contra-position of mimimulity of supermum required in Power Set Axiom - sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} - sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) + -- sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} + -- sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ ) minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) @@ -315,15 +315,14 @@ ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl ) ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) - union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} - union-u {X} {z} U>z = ord→od ( osuc ( od→ord z ) ) union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) - union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) - union← X z UX∋z = TransFiniteExists _ UX∋z - ( λ {y} xx not → not (ord→od y) (record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } )) + union← X z UX∋z = TransFiniteExists' _ lemma UX∋z where + lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) + lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } + -- ( λ {y} xx → ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y ψiso {ψ} t refl = t @@ -354,29 +353,12 @@ --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A -- - -- if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t - -- then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x - -- In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity of Ordinals -- ∩-≡ : { a b : OD {suc n} } → ({x : OD {suc n} } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) ∩-≡ {a} {b} inc = record { eq→ = λ {x} x<a → record { proj2 = x<a ; proj1 = def-subst {suc n} {_} {_} {b} {x} (inc (def-subst {suc n} {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; eq← = λ {x} x<a∩b → proj2 x<a∩b } - -- ord-power→ : (a : Ordinal ) ( t : OD) → Def (Ord a) ∋ t → {x : OD} → t ∋ x → Ord a ∋ x - -- ord-power→ a t P∋t {x} t∋x with osuc-≡< (sup-lb P∋t ) - -- ... | case1 eq = proj1 (def-subst t∋x (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl ) - -- ... | case2 lt = lemma3 where - -- sp = sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))) - -- minsup : OD - -- minsup = ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) - -- Ltx : {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x - -- Ltx {n} {x} {t} lt = c<→o< lt - -- -- lemma1 hold because a subset of ordinals is ordinal - -- lemma1 : od→ord t o< od→ord minsup → minsup ∋ Ord (od→ord t) - -- lemma1 lt = {!!} - -- lemma3 : od→ord x o< a - -- lemma3 = otrans (proj1 (lemma1 lt)) (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) -- -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t -- Power A is a sup of ZFSubset A t, so Power A ∋ t @@ -436,8 +418,6 @@ lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) - ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) - ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq regularity : (x : OD) (not : ¬ (x == od∅)) → (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) proj1 (regularity x not ) = x∋minimul x not @@ -454,7 +434,6 @@ eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d - infinity∅ : infinite ∋ od∅ {suc n} infinity∅ = def-subst {suc n} {_} {_} {infinite} {od→ord (od∅ {suc n})} iφ refl lemma where lemma : o∅ ≡ od→ord od∅