# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593916855 -32400
# Node ID 72f3e3b44c277cd587cf4ae79f462c78ab058e8a
# Parent  cde56f704eac6c55284b9038f1b38e1c6e9732f4
intoduce ωmax

diff -r cde56f704eac -r 72f3e3b44c27 OD.agda
--- a/OD.agda	Sun Jul 05 04:09:00 2020 +0900
+++ b/OD.agda	Sun Jul 05 11:40:55 2020 +0900
@@ -319,27 +319,18 @@
         isuc : {x : Ordinal  } →   infinite-d  x  →
                 infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
 
+    -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair.
+    -- We simply assumes nfinite-d y has a maximum.
+    -- 
+    -- This means that many of OD cannot be HODs because of the od→ord mapping divergence.
+    -- We should have some axioms to prevent this, but it may complicate thins.
+    -- 
+    postulate
+        ωmax : Ordinal
+        <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
+
     infinite : HOD 
-    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
-        u : HOD → HOD
-        u x = Union (x , (x , x))
-        lemma1 : {x : HOD} → u x ⊆ Union (u x , (u x , u x))   
-        lemma1 {x} = record { incl = λ {y} lt → lemma2 y lt } where
-            lemma2 : (y : HOD) → u x ∋ y → ((z : Ordinal) → (z ≡ od→ord (u x)) ∨ (z ≡ od→ord (u x , u x)) ∧ def (od (ord→od z)) (od→ord y) → ⊥) → ⊥
-            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
-        lemma6 : {x y : HOD} → y ≡ u x → HOD
-        lemma6 {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 {_} {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 = {!!}
+    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
 
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y