# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563487453 -32400
# Node ID c96f28c3c387f0e2dbc95c40bfb1cb1ede0f2811
# Parent  acbcbd98d5882409ffa85759ab0f15277750029b
...

diff -r acbcbd98d588 -r c96f28c3c387 HOD.agda
--- a/HOD.agda	Fri Jul 19 05:12:08 2019 +0900
+++ b/HOD.agda	Fri Jul 19 07:04:13 2019 +0900
@@ -18,7 +18,6 @@
     def : (x : Ordinal {n} ) → Set n
 
 open OD
-open import Data.Unit
 
 open Ordinal
 open _∧_
@@ -237,6 +236,30 @@
 -- L0 :  {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α
 -- L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n})  → L α ∋ x → L β ∋ x 
 
+-- another form of regularity 
+--
+{-# TERMINATING #-}
+ε-induction : {n m : Level} { ψ : OD {suc n} → Set m}
+     → ( {x : OD {suc n} } → ({ y : OD {suc n} } →  x ∋ y → ψ y ) → ψ x )
+     → (x : OD {suc n} ) → ψ x
+ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x))  <-osuc) where
+    ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox  → ψ (ord→od oy)
+    ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case1 ())
+    ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case2 ())
+    ε-induction-ord record { lv = lx ; ord = (OSuc lx ox) } {oy} y<x = 
+        ind {ord→od oy} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord (record { lv = lx ; ord = ox} ) (lemma y lt ))) where
+            lemma :  (y : OD) → ord→od oy ∋ y → od→ord y o< record { lv = lx ; ord = ox }
+            lemma y lt with osuc-≡< y<x
+            lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso
+            lemma y lt | case2 lt1 = ordtrans  (o<-subst (c<→o< lt) refl diso) lt1
+    ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {record { lv = ly ; ord = oy }} (case1 (s≤s x)) with <-cmp lx ly
+    ... | tri< a ¬b ¬c = ⊥-elim (lemma a x ) where  
+            lemma : {lx ly : Nat} → Suc lx ≤ ly → ly ≤ lx → ⊥
+            lemma (s≤s lt1) (s≤s lt2) = lemma lt1 lt2
+    ... | tri≈ ¬a refl ¬c = ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso ? 
+    ... | tri> ¬a ¬b c =  ε-induction-ord record { lv = lx ; ord = (Φ lx) }  (case1 c)
+
+
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
     ZFSet = OD {suc n}
@@ -467,23 +490,3 @@
          choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
          choice X {A} X∋A not = x∋minimul A not
 
-         -- another form of regularity 
-         --
-         ε-induction : {n m : Level} { ψ : OD {suc n} → Set m}
-              → ( {x : OD {suc n} } → ({ y : OD {suc n} } →  x ∋ y → ψ y ) → ψ x )
-              → (x : OD {suc n} ) → ψ x
-         ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x))  <-osuc) where
-             ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox  → ψ (ord→od oy)
-             ε-induction-ord ox = TransFinite {suc n} {suc n ⊔ m} {λ z → {oy : Ordinal {suc n} } → oy o< z  → ψ (ord→od oy) } lemma1 lemma2 ox where
-                lemma1 : (lx : Nat) {oy : Ordinal} → oy o< record { lv = lx ; ord = Φ lx } → ψ (ord→od oy)
-                lemma1 Zero {oy} (case1 ())
-                lemma1 Zero {oy} (case2 ())
-                lemma1 (Suc lx) {record { lv = Zero ; ord = Φ 0 }} (case1 (s≤s z≤n)) = {!!}
-                lemma1 (Suc lx) {record { lv = Zero ; ord = OSuc 0 oy }} (case1 (s≤s z≤n)) = {!!}
-                lemma1 (Suc (Suc lx)) {record { lv = Suc ly ; ord = Φ (Suc ly) }} (case1 (s≤s (s≤s x))) = {!!}
-                lemma1 (Suc (Suc lx)) {record { lv = Suc ly ; ord = OSuc (Suc ly) oy }} (case1 (s≤s (s≤s x))) = {!!}
-                lemma2 : (lx : Nat) (x₁ : OrdinalD lx) →
-                    ({oy : Ordinal} → oy o< record { lv = lx ; ord = x₁ } → ψ (ord→od oy)) →
-                    {oy : Ordinal} → oy o< record { lv = lx ; ord = OSuc lx x₁ } → ψ (ord→od oy)
-                lemma2 lx x1 p lt = ind ( λ {y} lty → subst (λ k → ψ k) oiso (p {!!} ))
-