### changeset 325:1a54dbe1ea4c

...
author Shinji KONO Sat, 04 Jul 2020 22:48:49 +0900 fbabb20f222e feeba7fd499a OD.agda ordinal.agda 2 files changed, 9 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Sat Jul 04 18:18:17 2020 +0900
+++ b/OD.agda	Sat Jul 04 22:48:49 2020 +0900
@@ -329,14 +329,17 @@
lemma2 y lt not = not (od→ord (u x)) record { proj1 = case1 refl ; proj2 = subst (λ k → def (od k) (od→ord y) ) (sym oiso) lt }
lemma3 : {x : HOD} → od→ord (u x) o< osuc (od→ord ( Union (u x , (u x , u x))   ))
lemma3 {x} = od⊆→o≤ lemma1
+        lemma4 : {x : HOD} → od→ord (u x) o< osuc (osuc (od→ord x))
+        lemma4 {x} = ordtrans (<odmax (x , x) {!!}) {!!}
lemma : {y : Ordinal} → infinite-d y → y o< next o∅
lemma {y} = TransFinite {λ x → infinite-d x → x o<  next o∅ } ind y where
ind : (x : Ordinal) → ((z : Ordinal) → z o< x → infinite-d z → z o< (next o∅))  →
infinite-d x → x o< (next  o∅)
ind o∅  prev iφ = proj1 next-limit
-           ind x prev (isuc lt) = lemma0 where
-              lemma0 : {x : Ordinal} → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
-              lemma0 {x} = {!!}
+           ind x prev (isuc lt) = lemma0 {_} {x} {!!} where
+              lemma0 : {x z : Ordinal} → x o< od→ord (Union (ord→od z , (ord→od z , ord→od z))) → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
+              lemma0 {x} with prev x {!!}
+              ... | t = {!!}

_=h=_ : (x y : HOD) → Set n
x =h= y  = od x == od y```
```--- a/ordinal.agda	Sat Jul 04 18:18:17 2020 +0900
+++ b/ordinal.agda	Sat Jul 04 22:48:49 2020 +0900
@@ -211,7 +211,7 @@
; o∅ = o∅
; osuc = osuc
; _o<_ = _o<_
-   ; next = ?
+   ; next = {!!}
; isOrdinal = record {
Otrans = ordtrans
; OTri = trio<
@@ -219,8 +219,8 @@
; <-osuc = <-osuc
; osuc-≡< = osuc-≡<
; TransFinite = TransFinite1
-     ; is-limit = ?
-     ; next-limit = ?
+     ; is-limit = {!!}
+     ; next-limit = {!!}
}
} where
ord1 : Set (suc n)```