Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal-definable.agda @ 87:296388c03358
split omax?
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 05 Jun 2019 07:05:48 +0900 |
parents | 4b2aff372b7c |
children | dccc9e2d1804 |
line wrap: on
line diff
--- a/ordinal-definable.agda Wed Jun 05 03:21:47 2019 +0900 +++ b/ordinal-definable.agda Wed Jun 05 07:05:48 2019 +0900 @@ -293,8 +293,8 @@ open _∧_ open Minimumo pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) - 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} + 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 ) } @@ -344,7 +344,7 @@ 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-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 + pair-osuc {x} {y} z with union← (x , x) y {!!} ... | t = {!!} next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x)) eq→ (next x ) {y} z = {!!} -- z : y o< osuc (osuc ox ) → y < osuc ox @@ -353,7 +353,7 @@ 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 osuc-≡< {suc n} (def-subst {suc n} (o<→c< z) oiso refl) + lemma1 with osuc-≡< {suc n} (def-subst {suc n} (o<→c< {!!}) oiso refl) lemma1 | case1 x = {!!} lemma1 | case2 t = {!!} -- = o<-subst (c<→o< {suc n} {_} {ord→od y} {!!} ) {!!} {!!}