Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal-definable.agda @ 81:96c932d0145d
simpler ordinal
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 04 Jun 2019 01:05:33 +0900 |
parents | 461690d60d07 |
children | 57814596a986 |
line wrap: on
line diff
--- a/ordinal-definable.agda Mon Jun 03 12:29:33 2019 +0900 +++ b/ordinal-definable.agda Tue Jun 04 01:05:33 2019 +0900 @@ -73,13 +73,9 @@ ∅1 {n} x (lift ()) ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} -∅3 {n} {x} = TransFinite {n} c1 c2 c3 x where +∅3 {n} {x} = TransFinite {n} c2 c3 x where c0 : Nat → Ordinal {n} → Set n c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x)) → x ≡ o∅ {n} - c1 : ∀ (lx : Nat ) → c0 lx (record { lv = Suc lx ; ord = ℵ lx } ) - c1 lx not with not ( record { lv = lx ; ord = Φ lx } ) - ... | t with t (case1 ≤-refl ) - c1 lx not | t | () c2 : (lx : Nat) → c0 lx (record { lv = lx ; ord = Φ lx } ) c2 Zero not = refl c2 (Suc lx) not with not ( record { lv = lx ; ord = Φ lx } ) @@ -92,9 +88,6 @@ c3 lx (OSuc .lx x₁) d not with not ( record { lv = lx ; ord = OSuc lx x₁ } ) ... | t with t (case2 (s< s<refl ) ) c3 lx (OSuc .lx x₁) d not | t | () - c3 (Suc lx) (ℵ lx) d not with not ( record { lv = Suc lx ; ord = OSuc (Suc lx) (Φ (Suc lx)) } ) - ... | t with t (case2 (s< ℵΦ< )) - c3 .(Suc lx) (ℵ lx) d not | t | () def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x def-subst df refl refl = df @@ -153,15 +146,6 @@ c≤-refl : {n : Level} → ( x : OD {n} ) → x c≤ x c≤-refl x = case1 refl -o<> : {n : Level } ( ox oy : Ordinal {n}) → ox o< oy → oy o< ox → ⊥ -o<> ox oy (case1 x<y) (case1 y<x) = >→¬< x<y y<x -o<> ox oy (case1 x<y) (case2 y<x) with d<→lv y<x -... | refl = =→¬< x<y -o<> ox oy (case2 x<y) (case1 y<x) with d<→lv x<y -... | refl = =→¬< y<x -o<> ox oy (case2 x<y) (case2 y<x) with d<→lv x<y -... | refl = trio<> x<y y<x - o<¬≡ : {n : Level } ( ox oy : Ordinal {n}) → ox ≡ oy → ox o< oy → ⊥ o<¬≡ ox ox refl (case1 lt) = =→¬< lt o<¬≡ ox ox refl (case2 (s< lt)) = trio<≡ refl lt @@ -186,14 +170,6 @@ ¬x<0 {n} {x} (case1 ()) ¬x<0 {n} {x} (case2 ()) --- o∅≡od∅0 : {n : Level} → ord→od (o∅ {suc n}) == od∅ {suc n} --- eq→ (o∅≡od∅0 {n} ) {x} y with c<→o< {suc n} {ord→od x} {ord→od (o∅ {suc n})} (def-subst {suc n} {_} {_} {ord→od o∅} {od→ord (ord→od x)} y refl (sym diso) ) --- eq→ (o∅≡od∅0 {n}) {x} y | lt = ⊥-elim ( ¬x<0 (o<-subst lt ord-iso diso ) ) --- eq← (o∅≡od∅0 {n}) {x} (lift ()) --- --- o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} --- o∅≡od∅ {n} = trans (cong (λ k → ord→od k ) ( ==→o≡ {n} (eq-trans o∅≡od∅0 (subst (λ k → od∅ == k ) (sym oiso) eq-refl )) ) ) oiso - o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} )) o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where @@ -207,7 +183,7 @@ o<→¬== {n} {x} {y} lt eq = o<→o> eq lt o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x ) -o<→¬c> {n} {x} {y} olt clt = o<> (od→ord x) (od→ord y) olt (c<→o< clt ) where +o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where o≡→¬c< : {n : Level} → { x y : OD {n} } → (od→ord x ) ≡ ( od→ord y) → ¬ x c< y o≡→¬c< {n} {x} {y} oeq lt = o<¬≡ (od→ord x) (od→ord y) (orefl oeq ) (c<→o< lt) @@ -270,7 +246,7 @@ ; Power = Power ; Select = Select ; Replace = Replace - ; infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero } ) + ; infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } ) ; isZF = isZF } where Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n} @@ -296,7 +272,7 @@ infixr 200 _∈_ infixr 230 _∩_ _∪_ infixr 220 _⊆_ - isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = ℵ Zero } )) + isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} )) isZF = record { isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } ; pair = pair @@ -368,15 +344,23 @@ 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 next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x)) - eq→ (next x ) {y} z = {!!} + eq→ (next x ) {y} z = {!!} eq← (next x ) {y} z = {!!} + next' : (x : OD) → ord→od ( od→ord ( Union (x , (x , x)))) == ord→od (osuc (od→ord x)) + next' x = subst ( λ k → k == ord→od (osuc (od→ord x))) (sym oiso) (next x) infinite : OD {suc n} - infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero } ) - infinity∅ : ord→od ( record { lv = Suc Zero ; ord = ℵ Zero } ) ∋ od∅ {suc n} + infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } ) + infinity∅ : ord→od ( record { lv = Suc Zero ; ord = Φ 1 } ) ∋ od∅ {suc n} infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅} (o<→c< ( case1 (s≤s z≤n ))) refl (cong (λ k → od→ord k) o∅≡od∅ ) infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) - infinity x ∞∋x = {!!} + infinity x ∞∋x = {!!} where + lemma : (ox : Ordinal {suc n} ) → ox o< record { lv = Suc Zero ; ord = Φ 1 } → osuc ox o< record { lv = Suc Zero ; ord = Φ 1 } + lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 {!!} + lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 {!!} + lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ())) + lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ())) + lemma record { lv = 1 ; ord = (Φ 1) } (case2 ℵΦ<) = case2 {!!} replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x replacement {ψ} X x = {!!}