Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 82:57814596a986

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Union (x , y) == (x , y ) only true on infinite case
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jun 2019 09:22:45 +0900
parents 96c932d0145d
children e013ccf00567
files ordinal-definable.agda
diffstat 1 files changed, 12 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Tue Jun 04 01:05:33 2019 +0900
+++ b/ordinal-definable.agda	Tue Jun 04 09:22:45 2019 +0900
@@ -343,8 +343,13 @@
          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-is-u : (x y : OD) → Union (x , y) ==  (x , y )
+         eq→ (pair-is-u x y) {w} z = def-subst (o<→c< ( ordtrans <-osuc z )) oiso diso
+         eq← (pair-is-u x y) {w} (case1 refl) =
+             def-subst (union→ (x , y) (ord→od w) (ord→od (osuc w)) ( record { proj1 = {!!} ; proj2 = {!!} } )) refl diso
+         eq← (pair-is-u x y) {w} (case2 refl) = {!!}
          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)
@@ -354,13 +359,15 @@
          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 = {!!} where
+         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 = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
+             lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)
              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 {!!}
+             lemma record { lv = 1 ; ord = (Φ 1) } (case2 c2) with d<→lv c2
+             lemma record { lv = (Suc Zero) ; ord = (Φ .1) } (case2 ()) | refl
          replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
          replacement {ψ} X x = {!!}