# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1594551337 -32400
# Node ID feb0fcc430a95db87597747567fd8e23fc6318a7
# Parent  bca043423554111f193dfded0a6c9ff1cef460d4
...

diff -r bca043423554 -r feb0fcc430a9 OD.agda
--- a/OD.agda	Sun Jul 12 12:32:42 2020 +0900
+++ b/OD.agda	Sun Jul 12 19:55:37 2020 +0900
@@ -103,12 +103,13 @@
   sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
   sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
 
---  another form of infinite
---  pair-ord< :  {x : Ordinal } → od→ord ( ord→od x , ord→od x ) o< next (od→ord x)
-
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
 
+-- possible restriction
+hod-ord< :  {x : HOD } → Set n
+hod-ord< {x} =  od→ord x o< next (odmax x)
+
 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
 ¬OD-order : ( od→ord : OD  → Ordinal ) → ( ord→od : Ordinal  → OD ) → ( { x y : OD  }  → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥
 ¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
@@ -221,6 +222,9 @@
     lemma {t} (case1 refl) = omax-x  _ _
     lemma {t} (case2 refl) = omax-y  _ _
 
+--  another form of infinite
+pair-ord< :  {x : Ordinal } → Set n
+pair-ord< {x} =  od→ord ( ord→od x , ord→od x ) o< next x
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
@@ -370,15 +374,23 @@
     infinite : HOD 
     infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
 
-    -- infinite' : HOD 
-    -- infinite' = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
-    --     u : (y : Ordinal ) → HOD
-    --     u y = Union (ord→od y , (ord→od y , ord→od y))
-    --     lemma : {y : Ordinal} → infinite-d y → y o< next o∅
-    --     lemma {o∅} iφ = {!!}
-    --     lemma (isuc {y} x) = {!!} where
-    --         lemma1 : od→ord (Union (ord→od y , (ord→od y , ord→od y))) o< od→ord (Union (u y , (u y , u y )))
-    --         lemma1 = {!!}
+    infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD 
+    infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
+        u : (y : Ordinal ) → HOD
+        u y = Union (ord→od y , (ord→od y , ord→od y))
+        lemma : {y : Ordinal} → infinite-d y → y o< next o∅
+        lemma {o∅} iφ = proj1  next-limit
+        lemma (isuc {y} x) = lemma2 where
+            lemma0 : y o< next o∅
+            lemma0 = lemma x
+            lemma3 : odef (u y ) y 
+            lemma3 = FExists _ (λ {z} t not → not (od→ord (ord→od y , ord→od y)) record { proj1 = case2 refl ; proj2 = lemma4 }) (λ not → not y (infinite-d y)) where
+                lemma4 : def (od (ord→od (od→ord (ord→od y , ord→od y)))) y 
+                lemma4 = subst₂ ( λ j k → def (od j) k ) (sym oiso) diso (case1 refl)
+            lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
+            lemma1 = ho<
+            lemma2 : od→ord (u y) o< next o∅
+            lemma2 = {!!}
         
 
     _=h=_ : (x y : HOD) → Set n
diff -r bca043423554 -r feb0fcc430a9 Ordinals.agda
--- a/Ordinals.agda	Sun Jul 12 12:32:42 2020 +0900
+++ b/Ordinals.agda	Sun Jul 12 19:55:37 2020 +0900
@@ -21,7 +21,8 @@
      <-osuc :  { x : ord  } → x o< osuc x
      osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
      not-limit :  ( x : ord  ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
-     next-limit : { y : ord } → (y o< next y ) ∧  ((x : ord) → x o< next y → osuc x o< next y )
+     next-limit : { y : ord } → (y o< next y ) ∧  ((x : ord) → x o< next y → osuc x o< next y ) ∧
+        ( (x : ord) → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z)  ))
      TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
@@ -219,6 +220,14 @@
           → ¬ p
         FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
+        next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
+        next< {x} {y} {z} x<nz y<nx with trio< y (next z)
+        next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
+        next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim ((proj2 (proj2 next-limit)) (next z) x<nz (subst (λ k → k o< next x) b y<nx)
+           (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (proj1 (proj2 next-limit) w (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
+        next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (proj2 (proj2 next-limit) (next z) x<nz (ordtrans c y<nx )
+           (λ w nz=ow → o<¬≡ (sym nz=ow) (proj1 (proj2 next-limit) _ (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
+
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field
             os→ : (x : Ordinal) → x o< maxordinal → Ordinal
diff -r bca043423554 -r feb0fcc430a9 ordinal.agda
--- a/ordinal.agda	Sun Jul 12 12:32:42 2020 +0900
+++ b/ordinal.agda	Sun Jul 12 19:55:37 2020 +0900
@@ -226,10 +226,19 @@
   } where
      next : Ordinal {suc n} → Ordinal {suc n}
      next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv))
-     next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y)
-     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = lemma } where
+     next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y) ∧
+        ( (x : Ordinal) → y o< x → x o< next y →  ¬ ((z : Ordinal) → ¬ (x ≡ osuc z)  ))
+     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = record { proj1 = lemma ; proj2 = lemma2 } } where
          lemma :  (x : Ordinal) → x o< next y → osuc x o< next y
          lemma x (case1 lt) = case1 lt
+         lemma2 : (x : Ordinal) → y o< x → x o< next y → ¬ ((z : Ordinal) → ¬ x ≡ osuc z)
+         lemma2 (ordinal Zero (Φ 0)) (case2 ()) (case1 (s≤s z≤n)) not
+         lemma2 (ordinal Zero (OSuc 0 dx)) (case2 Φ<) (case1 (s≤s z≤n)) not = not _ refl
+         lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl
+         lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl
+         lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where
+             lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
+             lemma3   (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n
      not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))
      not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () ))
      not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl )