Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 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 |
| files | ordinal-definable.agda ordinal.agda |
| diffstat | 2 files changed, 37 insertions(+), 132 deletions(-) [+] |
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 = {!!}
--- a/ordinal.agda Mon Jun 03 12:29:33 2019 +0900 +++ b/ordinal.agda Tue Jun 04 01:05:33 2019 +0900 @@ -11,27 +11,18 @@ data OrdinalD {n : Level} : (lv : Nat) → Set n where Φ : (lv : Nat) → OrdinalD lv OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv - ℵ_ : (lv : Nat) → OrdinalD (Suc lv) record Ordinal {n : Level} : Set n where field lv : Nat ord : OrdinalD {n} lv -data ¬ℵ {n : Level} {lx : Nat } : ( x : OrdinalD {n} lx ) → Set where - ¬ℵΦ : ¬ℵ (Φ lx) - ¬ℵs : {x : OrdinalD {n} lx } → ¬ℵ x → ¬ℵ (OSuc lx x) - -- -- Φ (Suc lv) < ℵ lv < OSuc (Suc lv) (ℵ lv) < OSuc ... < OSuc (Suc lv) (Φ (Suc lv)) < OSuc ... < ℵ (Suc lv) -- data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y - ℵΦ< : {lx : Nat} → Φ (Suc lx) d< (ℵ lx) - ℵ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → ¬ℵ x → OSuc (Suc lx) x d< (ℵ lx) - ℵs< : {lx : Nat} → (ℵ lx) d< OSuc (Suc lx) (ℵ lx) - ℵss< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → (ℵ lx) d< x → (ℵ lx) d< OSuc (Suc lx) x open Ordinal @@ -41,26 +32,14 @@ s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x s<refl {n} {lv} {Φ lv} = Φ< s<refl {n} {lv} {OSuc lv x} = s< s<refl -s<refl {n} {Suc lv} {ℵ lv} = ℵs< trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t -trio<> {_} {.(Suc _)} {.(OSuc (Suc _) (ℵ _))} {.(ℵ _)} ℵs< (ℵ< {_} {.(ℵ _)} ()) -trio<> {_} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} (ℵ< ()) ℵs< trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< () -trio<> {n} {.(Suc _)} {.(ℵ _)} {.(Φ (Suc _))} ℵΦ< () -trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (Φ (Suc _)))} (ℵ< ¬ℵΦ) (ℵss< ()) -trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} (ℵ< (¬ℵs x)) (ℵss< x<y) = trio<> (ℵ< x) x<y -trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (Φ (Suc _)))} {.(ℵ _)} (ℵss< ()) (ℵ< ¬ℵΦ) -trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} {.(ℵ _)} (ℵss< y<x) (ℵ< (¬ℵs x)) = trio<> y<x (ℵ< x) d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y d<→lv Φ< = refl d<→lv (s< lt) = refl -d<→lv ℵΦ< = refl -d<→lv (ℵ< _) = refl -d<→lv ℵs< = refl -d<→lv (ℵss< _) = refl o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x o<-subst df refl refl = df @@ -99,25 +78,10 @@ triO : {n : Level} → {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly ) triO {n} {lx} {ly} x y = <-cmp lx ly -fin : {n : Level} → {lx : Nat} → {y : OrdinalD {n} (Suc lx) } → y d< (ℵ lx) → ¬ℵ y -fin {_} {_} {Φ (Suc _)} ℵΦ< = ¬ℵΦ -fin {_} {_} {OSuc (Suc _) _} (ℵ< x) = ¬ℵs x - triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} ) triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d< -triOrdd {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d< triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) -triOrdd {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri< ℵΦ< (λ ()) ( λ lt → trio<> lt ℵΦ<) -triOrdd {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt ℵΦ< ) (λ ()) ℵΦ< -triOrdd {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y ) with triOrdd (ℵ lv) y -triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri< a ¬b ¬c = tri< (ℵss< a) (λ ()) (trio<> (ℵss< a) ) -triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri≈ ¬a refl ¬c = tri< ℵs< (λ ()) ( λ lt → trio<> lt ℵs< ) -triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt ( ℵ< (fin c)) ) (λ ()) ( ℵ< (fin c) ) triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ< -triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) with triOrdd x (ℵ lv) -triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri< a ¬b ¬c = tri< (ℵ< (fin a ) ) (λ ()) ( λ lt → trio<> lt (ℵ< (fin a ))) -triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri≈ ¬a refl ¬c = tri> (λ lt → trio<> lt ℵs< ) (λ ()) ℵs< -triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri> ¬a ¬b c = tri> (λ lt → trio<> lt (ℵss< c )) (λ ()) ( ℵss< c ) triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) ) ( λ lt → trio<> lt (s< a) ) triOrdd {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d< @@ -129,7 +93,6 @@ <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x <-osuc {n} {record { lv = lx ; ord = Φ .lx }} = case2 Φ< <-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s<refl ) -<-osuc {n} {record { lv = (Suc lx) ; ord = ℵ lx }} = case2 ℵs< osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x ) osuc-lveq {n} = refl @@ -140,73 +103,43 @@ nat-<≡ : { x : Nat } → x < x → ⊥ nat-<≡ (s≤s lt) = nat-<≡ lt +nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥ +nat-≡< refl lt = nat-<≡ lt + ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ ¬a≤a (s≤s lt) = ¬a≤a lt -xsyℵ : {n : Level} {lx : Nat} {x y : OrdinalD {n} lx } → x d< y → ¬ℵ y → ¬ℵ x -xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ -xsyℵ {_} {_} {OSuc lv₁ x} {OSuc lv₁ y} (s< x<y) (¬ℵs t) = ¬ℵs ( xsyℵ x<y t) -xsyℵ {_} {_} {OSuc .(Suc _) x} {.(ℵ _)} (ℵ< x₁) () -xsyℵ {_} {_} {ℵ lv₁} {.(OSuc (Suc lv₁) (ℵ lv₁))} ℵs< (¬ℵs t) = t -xsyℵ (ℵss< ()) (¬ℵs ¬ℵΦ) -xsyℵ (ℵss< x<y) (¬ℵs t) = xsyℵ x<y t +o<> : {n : Level} → {x y : Ordinal {n} } → y o< x → x o< y → ⊥ +o<> {n} {x} {y} (case1 x₁) (case1 x₂) = nat-<> x₁ x₂ +o<> {n} {x} {y} (case1 x₁) (case2 x₂) = nat-≡< (sym (d<→lv x₂)) x₁ +o<> {n} {x} {y} (case2 x₁) (case1 x₂) = nat-≡< (sym (d<→lv x₁)) x₂ +o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) (case2 ()) +o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y<x)) (case2 (s< x<y)) = + o<> (case2 y<x) (case2 x<y) orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n} lx } → x d< y → y d< z → x d< z orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< -orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< (ℵ< _) = ℵΦ< orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z ) -orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) (Φ (Suc lx)))} {.(ℵ lx)} (s< ()) (ℵ< ¬ℵΦ) -orddtrans ℵs< (ℵ< ()) -orddtrans {n} {Suc lx} {OSuc (Suc lx) x} {OSuc (Suc ly) y} {ℵ _} (s< x<y) (ℵ< t) = ℵ< ( xsyℵ x<y t ) -orddtrans {n} {.(Suc _)} {.(Φ (Suc _))} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} ℵΦ< ℵs< = Φ< -orddtrans {n} {.(Suc _)} {OSuc (Suc _) .(Φ (Suc _))} {.(ℵ _)} {OSuc (Suc _) (ℵ k)} (ℵ< ¬ℵΦ) ℵs< = s< ℵΦ< -orddtrans {n} {.(Suc _)} {OSuc (Suc lv) (OSuc (Suc _) x)} {ℵ lv} {.(OSuc (Suc _) (ℵ _))} (ℵ< (¬ℵs t)) ℵs< = s< ( ℵ< t ) -orddtrans {n} {.(Suc lv)} {ℵ lv} {OSuc .(Suc lv) (ℵ lv)} {OSuc .(Suc lv) .(OSuc (Suc lv) (ℵ lv))} ℵs< (s< ℵs<) = ℵss< ℵs< -orddtrans ℵΦ< (ℵss< y<z) = Φ< -orddtrans (ℵ< {lx} {Φ .(Suc lx)} nxx) (ℵss< {_} {k} y<z) = s< (orddtrans ℵΦ< y<z) -orddtrans (ℵ< {lx} {OSuc .(Suc lx) xx} (¬ℵs nxx)) (ℵss< y<z) = s< (orddtrans (ℵ< nxx) y<z) -orddtrans (ℵ< {.lv₁} {ℵ lv₁} ()) (ℵss< y<z) -orddtrans (ℵss< x<y) (s< y<z) = ℵss< ( orddtrans x<y y<z ) -orddtrans (ℵss< ()) (ℵ< ¬ℵΦ) -orddtrans (ℵss< ℵs<) (ℵ< (¬ℵs ())) -orddtrans (ℵss< (ℵss< x<y)) (ℵ< (¬ℵs x)) = orddtrans (ℵss< x<y) ( ℵ< x ) -orddtrans {n} {Suc lx} {x} {y} {z} ℵs< (s< (ℵss< {lx} {ss} y<z)) = ℵss< ( ℵss< y<z ) osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a → (x ≡ a ) ∨ (x o< a) osuc-≡< {n} {a} {x} (case1 lt) = case2 (case1 lt) osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case1 refl osuc-≡< {n} {record { lv = lv₁ ; ord = OSuc .lv₁ ord₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case2 (case2 Φ<) -osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(Φ (Suc lv₁)) }} (case2 Φ<) = case2 (case2 ℵΦ<) osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< ())) osuc-≡< {n} {record { lv = la ; ord = OSuc la oa }} {record { lv = la ; ord = (OSuc la ox) }} (case2 (s< lt)) with osuc-≡< {n} {record { lv = la ; ord = oa }} {record { lv = la ; ord = ox }} (case2 lt ) ... | case1 refl = case1 refl ... | case2 (case2 x) = case2 (case2( s< x) ) ... | case2 (case1 x) = ⊥-elim (¬a≤a x) where -osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(OSuc (Suc lv₁) (Φ (Suc lv₁))) }} (case2 (s< ℵΦ<)) = case2 (case2 (ℵ< ¬ℵΦ )) -osuc-≡< {n} {record { lv = (Suc lx) ; ord = ℵ lx }} {record { lv = (Suc lx) ; ord = (OSuc (Suc lx) (OSuc (Suc lx) ox)) }} (case2 (s< (ℵ< x))) with - osuc-≡< {n} {record { lv = (Suc lx) ; ord = ℵ lx }} {record { lv = (Suc lx) ; ord = (OSuc (Suc lx) ox) }} (case2 (lemma (ℵ< x)) ) where - lemma : OSuc (Suc lx) ox d< (ℵ lx) → OSuc (Suc lx) ox d< ord (osuc (record { lv = Suc lx ; ord = ℵ lx })) - lemma lt = orddtrans lt s<refl -... | case1 () -... | case2 ttt = case2 ( case2 (ℵ< (¬ℵs x) )) -osuc-≡< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 ℵs<) = case1 refl -osuc-≡< {n} {record { lv = .(Suc _) ; ord = Φ .(Suc _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< lt)) = case2 (case2 lt) -osuc-≡< {n} {record { lv = .(Suc _) ; ord = OSuc .(Suc _) ord₁ }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< lt)) = case2 (case2 lt) -osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(ℵ lv₁) }} (case2 (ℵss< lt)) = case1 refl osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥ osuc-< {n} {x} {y} y<ox x<y with osuc-≡< y<ox osuc-< {n} {x} {x} y<ox (case1 x₁) | case1 refl = ⊥-elim (¬a≤a x₁) osuc-< {n} {x} {x} (case1 x₂) (case2 x₁) | case1 refl = ⊥-elim (¬a≤a x₂) osuc-< {n} {x} {x} (case2 x₂) (case2 x₁) | case1 refl = ≡→¬d< x₁ -osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₁ x₂ -osuc-< {n} {x} {y} y<ox (case2 x₂) | case2 (case1 x₁) with d<→lv x₂ -... | refl = ⊥-elim (¬a≤a x₁) -osuc-< {n} {x} {y} y<ox (case1 x₁) | case2 (case2 y<x) with d<→lv y<x -... | refl = ⊥-elim (¬a≤a x₁) -osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 (case2 y<x) with d<→lv y<x | d<→lv x<y -... | refl | refl = trio<> y<x x<y +osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₂ x₁ +osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case2 x₁) = nat-≡< (sym (d<→lv x₁)) x₂ +osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 y<x = o<> (case2 x<y) y<x max : (x y : Nat) → Nat max Zero Zero = Zero @@ -231,26 +164,23 @@ ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ ) -ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂ +ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂ ... | refl = case1 x₁ -ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁ +ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁ ... | refl = case1 x₂ ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂ ... | refl | refl = case2 ( orddtrans x₁ x₂ ) - trio< : {n : Level } → Trichotomous {suc n} _≡_ _o<_ trio< a b with <-cmp (lv a) (lv b) trio< a b | tri< a₁ ¬b ¬c = tri< (case1 a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a) lemma1 (case1 x) = ¬c x - lemma1 (case2 x) with d<→lv x - lemma1 (case2 x) | refl = ¬b refl + lemma1 (case2 x) = ⊥-elim (nat-≡< (sym ( d<→lv x )) a₁ ) trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b) lemma1 (case1 x) = ¬a x - lemma1 (case2 x) with d<→lv x - lemma1 (case2 x) | refl = ¬b refl + lemma1 (case2 x) = ⊥-elim (nat-≡< (sym ( d<→lv x )) c ) trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b ) trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where lemma1 : (record { lv = _ ; ord = x }) ≡ b → x ≡ ord b @@ -273,13 +203,7 @@ OrdTrans (case1 refl) (case1 refl) = case1 refl OrdTrans (case1 refl) (case2 lt2) = case2 lt2 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 -OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) ) -OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y -OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x ) -OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x -OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y) -OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y -OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y )) +OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n) OrdPreorder {n} = record { Carrier = Ordinal @@ -293,12 +217,9 @@ } TransFinite : {n : Level} → { ψ : Ordinal {n} → Set n } - → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) → ∀ (x : Ordinal) → ψ x -TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv -TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁ - ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } )) -TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁ - +TransFinite caseΦ caseOSuc record { lv = lv ; ord = (Φ (lv)) } = caseΦ lv +TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = + caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox })