Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal-definable.agda @ 84:4b2aff372b7c
omax ..
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 04 Jun 2019 23:58:58 +0900 |
parents | e013ccf00567 |
children | 296388c03358 |
line wrap: on
line diff
--- 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))