# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593781081 -32400
# Node ID 21203fe0342f45776b2c0410a0631c67a4c3bb00
# Parent  eef432aa8dfb1c80399cd718ebc75a92306ab9b3
infinite ...

diff -r eef432aa8dfb -r 21203fe0342f OD.agda
--- 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
diff -r eef432aa8dfb -r 21203fe0342f Ordinals.agda
--- 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