# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1568680167 -32400
# Node ID d9d178d1457cfae6e93ca511d4b7188eab3b12a6
# Parent  8b85949bde00dfb7e6643ceda0fb518fd1bb65c8
ε-induction from TransFinite induction

diff -r 8b85949bde00 -r d9d178d1457c OD.agda
--- a/OD.agda	Thu Sep 05 10:58:06 2019 +0900
+++ b/OD.agda	Tue Sep 17 09:29:27 2019 +0900
@@ -350,6 +350,17 @@
     ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
    } 
 
+open import Data.Unit
+
+ε-induction : { ψ : OD  → Set (suc n)}
+   → ( {x : OD } → ({ y : OD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : OD ) → ψ x
+ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
+     ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
+
 OD→ZF : ZF  
 OD→ZF   = record { 
     ZFSet = OD 
diff -r 8b85949bde00 -r d9d178d1457c ordinal.agda
--- a/ordinal.agda	Thu Sep 05 10:58:06 2019 +0900
+++ b/ordinal.agda	Tue Sep 17 09:29:27 2019 +0900
@@ -241,68 +241,3 @@
   open OD (C-Ordinal {n})
   open OD.OD
   
-  --
-  -- another form of regularity 
-  --
-  ε-induction : {m : Level} { ψ : OD  → Set m}
-   → ( {x : OD } → ({ y : OD } →  x ∋ y → ψ y ) → ψ x )
-   → (x : OD ) → ψ x
-  ε-induction {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x)))  <-osuc) where
-    ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
-      → (ly < lx) ∨ (oy d< ox  ) → ψ (ord→od (record { lv = ly ; ord = oy } ) )
-    ε-induction-ord lx  (OSuc lx ox) {ly} {oy} y<x = 
-      ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where
-          lemma :  (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox }
-          lemma z lt with osuc-≡< y<x
-          lemma z lt | case1 refl = o<-subst (c<→o< lt) refl diso
-          lemma z lt | case2 lt1 = ordtrans  (o<-subst (c<→o< lt) refl diso) lt1  
-    ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) =                    
-      ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt )  where  
-          --
-          --     if lv of z if less than x Ok
-          --     else lv z = lv x. We can create OSuc of z which is larger than z and less than x in lemma
-          --
-          --                         lx    Suc lx      (1) lz(a) <lx by case1
-          --                 ly(1)   ly(2)             (2) lz(b) <lx by case1
-          --           lz(a) lz(b)   lz(c)                 lz(c) <lx by case2 ( ly==lz==lx)
-          --
-          lemma0 : { lx ly : Nat } → ly < Suc lx  → lx < ly → ⊥
-          lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2
-          lemma1 : {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly
-          lemma1  {ly} {oy} = let open ≡-Reasoning in begin
-                  lv (od→ord (ord→od (record { lv = ly ; ord = oy })))
-               ≡⟨ cong ( λ k → lv k ) diso ⟩
-                  lv (record { lv = ly ; ord = oy })
-               ≡⟨⟩
-                  ly
-               ∎
-          lemma :  (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z
-          lemma z lt with  c<→o<  {z} {ord→od (record { lv = ly ; ord = oy })} lt
-          lemma z lt | case1 lz<ly with <-cmp lx ly
-          lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
-          lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c =    -- ly(1)
-                subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) ))
-          lemma z lt | case1 lz<ly | tri> ¬a ¬b c =       -- lz(a)
-                subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c))))
-          lemma z lt | case2 lz=ly with <-cmp lx ly
-          lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
-          lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly        -- lz(b)
-          ... | eq = subst (λ k → ψ k ) oiso
-               (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c )))
-          lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly    -- lz(c)
-          ... | eq =  subst (λ k → ψ k ) oiso ( ε-induction-ord lx (dz oz=lx) {lv (od→ord z)} {ord (od→ord z)} (case2 (dz<dz oz=lx) )) where
-              oz=lx : lv (od→ord z) ≡ lx 
-              oz=lx = let open ≡-Reasoning in begin
-                  lv (od→ord z)
-                 ≡⟨ eq ⟩
-                  lv (od→ord (ord→od (ordinal ly oy)))
-                 ≡⟨ cong ( λ k → lv k ) diso ⟩
-                  lv (ordinal ly oy)
-                 ≡⟨ sym lx=ly  ⟩
-                  lx
-                 ∎
-              dz : lv (od→ord z) ≡ lx → OrdinalD lx
-              dz refl = OSuc lx (ord (od→ord z))
-              dz<dz  : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x
-              dz<dz refl = s<refl 
-