# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593854297 -32400
# Node ID fbabb20f222ef021d811d5f5499ce44a93fe28b1
# Parent  e228e96965f0930d72f4f92ebe10a172dfc13b37
...

diff -r e228e96965f0 -r fbabb20f222e OD.agda
--- a/OD.agda	Sat Jul 04 12:53:40 2020 +0900
+++ b/OD.agda	Sat Jul 04 18:18:17 2020 +0900
@@ -132,6 +132,7 @@
    lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y
    lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt )
 
+
 _∋_ : ( a x : HOD  ) → Set n
 _∋_  a x  = odef a ( od→ord x )
 
@@ -240,6 +241,9 @@
     ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } 
    } 
 
+od⊆→o≤  : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
+od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
+
 power< : {A x : HOD  } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
 power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) diso (lemma y x∋y ) ) where
     lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
@@ -247,7 +251,7 @@
 
 open import Data.Unit
 
-ε-induction : { ψ : HOD  → Set (suc n)}
+ε-induction : { ψ : HOD  → Set n}
    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
    → (x : HOD ) → ψ x
 ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
@@ -315,20 +319,24 @@
         isuc : {x : Ordinal  } →   infinite-d  x  →
                 infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
 
-    is-ω : (x : Ordinal) → Dec (infinite-d x )
-    is-ω x = {!!}
-
     infinite : HOD 
-    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma1 } where
-        lemma : {y : Ordinal} → Lift (suc n) (infinite-d y → y o< next o∅ )
-        lemma {y} = TransFinite {λ x → Lift (suc n) (infinite-d x → x o<  next o∅) } ind y where
-           ind : (x : Ordinal) → ((z : Ordinal) → z o< x → Lift (suc n) (infinite-d z → z o< (next o∅)))  →
-                Lift (suc n) (infinite-d x → x o< (next  o∅))
-           ind x prev with {!!}
-           ... | ttt = {!!}
-        lemma1 : {y : Ordinal} → infinite-d y → y o< next o∅ 
-        lemma1 {y} with lemma {y}
-        lemma1 {y} | lift p = p
+    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
+        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} = {!!}
 
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y
diff -r e228e96965f0 -r fbabb20f222e Ordinals.agda
--- a/Ordinals.agda	Sat Jul 04 12:53:40 2020 +0900
+++ b/Ordinals.agda	Sat Jul 04 18:18:17 2020 +0900
@@ -22,7 +22,7 @@
      osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
      is-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 )
-     TransFinite : { ψ : ord  → Set (suc n) }
+     TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
 
diff -r e228e96965f0 -r fbabb20f222e ordinal.agda
--- a/ordinal.agda	Sat Jul 04 12:53:40 2020 +0900
+++ b/ordinal.agda	Sat Jul 04 18:18:17 2020 +0900
@@ -211,6 +211,7 @@
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
+   ; next = ?
    ; isOrdinal = record {
        Otrans = ordtrans
      ; OTri = trio<
@@ -218,14 +219,16 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
+     ; is-limit = ?
+     ; next-limit = ?
    }
   } where
      ord1 : Set (suc n)
      ord1 = Ordinal {suc n}
-     TransFinite1 : { ψ : ord1  → Set (suc (suc n)) }
+     TransFinite1 : { ψ : ord1  → Set (suc n) }
           → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord1)  → ψ x
-     TransFinite1 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+     TransFinite1 {ψ} lt x = TransFinite {n} {suc n} {ψ} caseΦ caseOSuc x where
         caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
             ψ (record { lv = lx ; ord = Φ lx })
         caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
diff -r e228e96965f0 -r fbabb20f222e zf.agda
--- a/zf.agda	Sat Jul 04 12:53:40 2020 +0900
+++ b/zf.agda	Sat Jul 04 18:18:17 2020 +0900
@@ -49,7 +49,7 @@
      -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
      -- regularity without minimum
-     ε-induction : { ψ : ZFSet → Set (suc m)}
+     ε-induction : { ψ : ZFSet → Set m}
               → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
               → (x : ZFSet ) → ψ x
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )