### changeset 320:21203fe0342f

infinite ...
author Shinji KONO Fri, 03 Jul 2020 21:58:01 +0900 eef432aa8dfb a81824502ebd OD.agda Ordinals.agda 2 files changed, 15 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Fri Jul 03 21:39:10 2020 +0900
+++ b/OD.agda	Fri Jul 03 21:58:01 2020 +0900
@@ -308,7 +308,12 @@
infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))

infinite : HOD
-    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = {!!} ; <odmax = {!!} }
+    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
+        lemma : {y : Ordinal} → infinite-d y → y o< next o∅
+        lemma {o∅} iφ = proj1 next-limit
+        lemma {n} (isuc i) = {!!} where
+            lemma1 = proj2 next-limit
+

_=h=_ : (x y : HOD) → Set n
x =h= y  = od x == od y```
```--- a/Ordinals.agda	Fri Jul 03 21:39:10 2020 +0900
+++ b/Ordinals.agda	Fri Jul 03 21:58:01 2020 +0900
@@ -13,14 +13,15 @@
open import Relation.Binary
open import Relation.Binary.Core

-record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
+record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
field
Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
OTri : Trichotomous {n} _≡_  _o<_
¬x<0 :   { x  : ord  } → ¬ ( x o< o∅  )
<-osuc :  { x : ord  } → x o< osuc x
osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)
-     is-limit :  { x : ord  } → Dec ( ¬ ((y : ord) → x ≡ osuc y) )
+     is-limit :  ( x : ord  ) → Dec ( ¬ ((y : ord) → x ≡ osuc y) )
+     next-limit : { x : ord } → (x o< next x )∧ (¬ ((y : ord) → next x ≡ osuc y) )
TransFinite : { ψ : ord  → Set (suc n) }
→ ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
→  ∀ (x : ord)  → ψ x
@@ -32,7 +33,8 @@
o∅ : ord
osuc : ord → ord
_o<_ : ord → ord → Set n
-     isOrdinal : IsOrdinals ord o∅ osuc _o<_
+     next :  ord → ord
+     isOrdinal : IsOrdinals ord o∅ osuc _o<_ next

module inOrdinal  {n : Level} (O : Ordinals {n} ) where

@@ -48,10 +50,14 @@
o∅ :   Ordinal
o∅ = Ordinals.o∅ O

+        next :   Ordinal → Ordinal
+        next = Ordinals.next O
+
¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
<-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
+        next-limit = IsOrdinals.next-limit  (Ordinals.isOrdinal O)

o<-dom :   { x y : Ordinal } → x o< y → Ordinal
o<-dom  {x} _ = x```