# HG changeset patch # User Shinji KONO # Date 1559660338 -32400 # Node ID 4b2aff372b7c6f3242497f78ae311fbddf718dbf # Parent e013ccf005672d8703eb6b59d0395df527a8405d omax .. diff -r e013ccf00567 -r 4b2aff372b7c ordinal-definable.agda --- a/ordinal-definable.agda Tue Jun 04 12:28:43 2019 +0900 +++ b/ordinal-definable.agda Tue Jun 04 23:58:58 2019 +0900 @@ -254,7 +254,7 @@ Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n} Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } _,_ : OD {suc n} → OD {suc n} → OD {suc n} - x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) } + x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) } Union : OD {suc n} → OD {suc n} Union U = record { def = λ y → osuc y o< (od→ord U) } -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) @@ -293,8 +293,8 @@ open _∧_ open Minimumo pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) - proj1 (pair A B ) = case1 refl - proj2 (pair A B ) = case2 refl + proj1 (pair A B ) = omax-x {n} {od→ord A} {od→ord B} + proj2 (pair A B ) = omax-y {n} {od→ord A} {od→ord B} empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) empty x () --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x ) } @@ -343,29 +343,20 @@ extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 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 - pair-or : {x y : OD {suc n} } → (x , x) ∋ y → (y == x ) ∨ (x ∋ y ) - pair-or {x} {y} lt with tri-c< x y - pair-or {x} {y} lt | tri< a ¬b ¬c = {!!} -- x < y < ( x , x ) - pair-or {x} {y} lt | tri≈ ¬a b ¬c = case1 (eq-sym b) - pair-or {x} {y} lt | tri> ¬a ¬b c = case2 c - pair-osuc : (x : OD) → od→ord (x , x) ≡ osuc (od→ord x) - pair-osuc x with trio< (od→ord (x , x)) (osuc (od→ord x)) - pair-osuc x | tri< a ¬b ¬c = ⊥-elim ( osuc-< a (c<→o< (proj1 (pair x x )) )) - pair-osuc x | tri≈ ¬a b ¬c = b - pair-osuc x | tri> ¬a ¬b c with pair-or (def-subst (o<→c< c ) oiso refl ) -- (x , x) ∋ ord→od (osuc (od→ord x) ) - pair-osuc x | tri> ¬a ¬b c | case1 eq = ⊥-elim ( o<→¬== (def-subst {suc n} (o<→c< c ) refl diso ) eq ) - pair-osuc x | tri> ¬a ¬b c | case2 lt = ⊥-elim (c<> c lt ) where - lemma2 : (z : Ordinal {suc n} ) → lv (od→ord (ord→od z , ord→od z) ) ≡ lv z - lemma2 z = {!!} + pair-osuc : {x y : OD {suc n}} → (x , x) ∋ y → (od→ord y ) o< osuc (od→ord x) + pair-osuc {x} {y} z with union← (x , x) y z + ... | t = {!!} next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x)) - eq→ (next x ) {y} z = {!!} + eq→ (next x ) {y} z = {!!} -- z : y o< osuc (osuc ox ) → y < osuc ox eq← (next x ) {y} z = def-subst {suc n} {_} {_} {Union (x , (x , x))} {_} (union→ (x , (x , x)) (ord→od y) (ord→od (osuc y)) (record { proj1 = lemma1 ; proj2 = lemma2 } )) refl diso where + lemma0 : (x , x) ∋ ord→od y + lemma0 = o<-subst {suc n} {od→ord (ord→od y)} {od→ord {!!}} (c<→o< z) {!!} {!!} lemma1 : (x , (x , x)) ∋ ord→od (osuc y) -- z : def (ord→od (osuc (od→ord x))) y - lemma1 with tri-c< (x , x) (ord→od (osuc (od→ord x))) - lemma1 | tri< a ¬b ¬c = {!!} - lemma1 | tri≈ ¬a b ¬c = {!!} - lemma1 | tri> ¬a ¬b c = {!!} + lemma1 with osuc-≡< {suc n} (def-subst {suc n} (o<→c< z) oiso refl) + lemma1 | case1 x = {!!} + lemma1 | case2 t = {!!} + -- = o<-subst (c<→o< {suc n} {_} {ord→od y} {!!} ) {!!} {!!} lemma2 : ord→od (osuc y) ∋ ord→od y lemma2 = o<→c< <-osuc next' : (x : OD) → ord→od ( od→ord ( Union (x , (x , x)))) == ord→od (osuc (od→ord x)) diff -r e013ccf00567 -r 4b2aff372b7c ordinal.agda --- a/ordinal.agda Tue Jun 04 12:28:43 2019 +0900 +++ b/ordinal.agda Tue Jun 04 23:58:58 2019 +0900 @@ -153,12 +153,6 @@ maxαd x y | tri≈ ¬a b ¬c = x maxαd x y | tri> ¬a ¬b c = x -maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal -maxα x y with <-cmp (lv x) (lv y) -maxα x y | tri< a ¬b ¬c = x -maxα x y | tri> ¬a ¬b c = y -maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) } - _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n) a o≤ b = (a ≡ b) ∨ ( a o< b ) @@ -199,6 +193,38 @@ lemma1 (case1 x) = ¬a x lemma1 (case2 x) = ≡→¬d< x +maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal +maxα x y with <-cmp (lv x) (lv y) +maxα x y | tri< a ¬b ¬c = x +maxα x y | tri> ¬a ¬b c = y +maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) } + +omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n} +omax {n} x y with <-cmp (lv x) (lv y) +omax {n} x y | tri< a ¬b ¬c = osuc y +omax {n} x y | tri> ¬a ¬b c = osuc x +omax {n} x y | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y) +omax {n} x y | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = osuc y +omax {n} x y | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = osuc x +omax {n} x y | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = osuc x + +omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y +omax< {n} x y lt with <-cmp (lv x) (lv y) +omax< {n} x y lt | tri< a ¬b ¬c = refl +omax< {n} x y (case1 lt) | tri> ¬a ¬b c = ⊥-elim (¬a lt) +omax< {n} x y (case2 lt) | tri> ¬a ¬b c = ⊥-elim (¬b (d<→lv lt )) +omax< {n} x y (case1 lt) | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) +omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord y) +omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = refl +omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri≈ ¬a₁ b ¬c₁ = ⊥-elim ( trio<≡ b lt ) +omax< {n} x y (case2 lt) | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim ( o<> (case2 lt) (case2 c) ) + +omaxx : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y +omaxx {n} x y with trio< x y +omaxx {n} x y | tri< a ¬b ¬c = {!!} +omaxx {n} x y | tri> ¬a ¬b c = {!!} +omaxx {n} x y | tri≈ ¬a b ¬c = {!!} + OrdTrans : {n : Level} → Transitive {suc n} _o≤_ OrdTrans (case1 refl) (case1 refl) = case1 refl OrdTrans (case1 refl) (case2 lt2) = case2 lt2