Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 65:164ad5a703d8
¬∅=→∅∈ : {n : Level} → { x : OD {suc n} } → ¬ ( x == od∅ {suc n} ) → x ∋ od∅ {suc n}
¬∅=→∅∈ {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where
lemma : (ox : Ordinal {suc n}) → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n}
lemma ox = TransFinite {suc n} {λ ox → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} } { }0 { }1 { }2 ox
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 30 May 2019 01:02:47 +0900 |
| parents | 87df00599a0e |
| children | 92a11dc6425c |
| files | ordinal-definable.agda zf.agda |
| diffstat | 2 files changed, 20 insertions(+), 23 deletions(-) [+] |
line wrap: on
line diff
--- a/ordinal-definable.agda Wed May 29 18:50:57 2019 +0900 +++ b/ordinal-definable.agda Thu May 30 01:02:47 2019 +0900 @@ -221,6 +221,16 @@ tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) (ord→== b) (o≡→¬c< (sym b)) tri-c< {n} x y | tri> ¬a ¬b c = tri> ( o<→¬c> c) (λ eq → o<→¬== c (eq-sym eq ) ) (def-subst (o<→c< c) oiso diso) +¬∅=→∅∈ : {n : Level} → { x : OD {suc n} } → ¬ ( x == od∅ {suc n} ) → x ∋ od∅ {suc n} +¬∅=→∅∈ {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where + lemma : (ox : Ordinal {suc n}) → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} + lemma ox = TransFinite {suc n} {λ ox → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} } {!!} {!!} {!!} ox + +-- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc (suc n)) (suc (suc n )) + +-- ==∅→≡ : {n : Level} → { x : OD {suc n} } → ( x == od∅ {suc n} ) → x ≡ od∅ {suc n} +-- ==∅→≡ {n} {x} eq = cong ( λ k → record { def = k } ) (trans {!!} ∅-base-def ) where + c<> : {n : Level } { x y : OD {suc n}} → x c< y → y c< x → ⊥ c<> {n} {x} {y} x<y y<x with tri-c< x y c<> {n} {x} {y} x<y y<x | tri< a ¬b ¬c = ¬c y<x @@ -317,7 +327,7 @@ ; empty = empty ; power→ = {!!} ; power← = {!!} - ; extentionality = {!!} + ; extensionality = {!!} ; minimul = minimul ; regularity = regularity ; infinity∅ = {!!} @@ -345,7 +355,7 @@ } ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq - minord : (x : OD {suc n} ) → ¬ (x == od∅ )→ Minimumo (od→ord x) + minord : (x : OD {suc n} ) → ¬ (x == od∅ ) → Minimumo (od→ord x) minord x not = ominimal (od→ord x) (∅9 not) minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} minimul x not = ord→od ( mino (minord x not)) @@ -353,29 +363,16 @@ omin→cmin {x} {not} m<x = def-subst {suc n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl minimul<x : (x : OD {suc n} ) → (not : ¬ x == od∅ ) → x ∋ minimul x not minimul<x x not = omin→cmin {x} {not} (min<x (minord x not)) - omin∅≡min∅ : (ox : Ordinal {suc n}) → {not : ¬ ( ord→od ox == od∅)} - → mino (ominimal ox (∅10 refl not)) ≡ mino (ominimal (od→ord (ord→od ox)) (∅9 not)) - omin∅≡min∅ ox {not} with ominimal ox (∅10 refl not) - omin∅≡min∅ record { lv = Zero ; ord = (Φ .0) } | record { mino = mino ; min<x = case1 () } - omin∅≡min∅ record { lv = Zero ; ord = (Φ .0) } | record { mino = mino ; min<x = case2 () } - omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) } | record { mino = _ ; min<x = case1 () } - omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) } | record { mino = record { lv = 0 ; ord = Φ 0 } ; min<x = case2 Φ< } = {!!} - omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) } {_} | record { mino = record { lv = .0 ; ord = .(OSuc 0 _) } ; min<x = case2 (s< x)} = {!!} - omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!} - omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } | record { mino = mino ; min<x = case2 () } - omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!} - omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } | record { mino = _ ; min<x = case2 lt } = {!!} - omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) } | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!} - omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) } | record { mino = _ ; min<x = case2 lt } = {!!} - omin∅≡min∅ record { lv = (Suc lv₁) ; ord = ord } {not} | record { mino = mino ; min<x = min<x } = {!!} - omin∅→min∅ : (ox : Ordinal {suc n}) { x : OD {suc n} } → {not : ¬ ( ord→od ox == od∅)} + omin∅→min∅ : (ox : Ordinal {suc n}) → {not : ¬ ( ord→od ox == od∅)} → mino (ominimal ox (∅10 refl not)) ≡ o∅ → mino (ominimal (od→ord (ord→od ox)) (∅9 not)) ≡ o∅ - omin∅→min∅ ox {x} {not} eq with ominimal ox (∅10 refl not) + omin∅→min∅ ox {not} eq with ominimal ox (∅10 refl not) omin∅→min∅ record { lv = Zero ; ord = (Φ .0) } eq | record { mino = mino ; min<x = case1 () } omin∅→min∅ record { lv = Zero ; ord = (Φ .0) } eq | record { mino = mino ; min<x = case2 () } omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) } refl | record { mino = .o∅ ; min<x = case1 () } - omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) } refl | record { mino = .o∅ ; min<x = case2 Φ< } = - subst (λ k → ? ≡ k ) ? (omin∅→min∅ o∅ {!!}) + omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 (Φ .0)) } {not} refl | record { mino = record { lv = .0 ; ord = .(Φ 0) } ; min<x = case2 Φ< } = {!!} where + lemma : mino (ominimal (od→ord (ord→od (record { lv = Zero ; ord = OSuc Zero (Φ Zero) }))) (∅5 (λ eq → not (∅7 eq)))) ≡ o∅ + lemma = {!!} + omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 (OSuc .0 ord₁)) } {_} refl | record { mino = record { lv = .0 ; ord = .(Φ 0) } ; min<x = case2 Φ< } = {!!} omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!} omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } eq | record { mino = mino ; min<x = case2 () } omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
--- a/zf.agda Wed May 29 18:50:57 2019 +0900 +++ b/zf.agda Thu May 30 01:02:47 2019 +0900 @@ -68,8 +68,8 @@ -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) power→ : ∀( A t : ZFSet ) → Power A ∋ t → ∀ {x} → _⊆_ t A {x} power← : ∀( A t : ZFSet ) → ∀ {x} → _⊆_ t A {x} → Power A ∋ t - -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) - extentionality : ( A B z : ZFSet ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B + -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) + extensionality : ( A B z : ZFSet ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet regularity : ∀( x : ZFSet ) → (not : ¬ (x ≈ ∅)) → ( minimul x not ∈ x ∧ ( minimul x not ∩ x ≈ ∅ ) )