# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1596292630 -32400
# Node ID cc7909f86841eab6a6fbecbd727c345b4411f90a
# Parent  9984cdd88da335dbfad5cdeb3f6e474cdcdc7174
remvoe TransFinifte1

diff -r 9984cdd88da3 -r cc7909f86841 BAlgbra.agda
--- a/BAlgbra.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/BAlgbra.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -4,7 +4,9 @@
 
 open import zf
 open import logic
+import OrdUtil
 import OD 
+import ODUtil
 import ODC
 
 open import Relation.Nullary
@@ -16,6 +18,12 @@
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ )  
 
 open inOrdinal O
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
 open OD O
 open OD.OD
 open ODAxiom odAxiom
@@ -47,7 +55,7 @@
         lemma4 {y} z with proj1 z
         lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) *iso (proj2 z)) )
         lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) *iso (proj2 z)) )
-        lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x
+        lemma3 : (((u : Ordinal ) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x
         lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not)   -- choice
     lemma2 :  {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
     lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A
diff -r 9984cdd88da3 -r cc7909f86841 LEMC.agda
--- a/LEMC.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/LEMC.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -20,6 +20,13 @@
 open OD.OD
 open OD._==_
 open ODAxiom odAxiom
+import OrdUtil
+import ODUtil
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
 
 open import zfc
 
@@ -89,7 +96,7 @@
                  ψ : ( ox : Ordinal ) → Set n
                  ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced (& X)
                  lemma-ord : ( ox : Ordinal  ) → ψ ox
-                 lemma-ord  ox = TransFinite {ψ} induction ox where
+                 lemma-ord  ox = TransFinite0 {ψ} induction ox where
                     ∀-imply-or :  {A : Ordinal  → Set n } {B : Set n }
                         → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
                     ∀-imply-or  {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM
@@ -107,13 +114,15 @@
                          lemma1 y with ∋-p X (* y)
                          lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } )
                          lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) )
-                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (& X)
+                         lemma :  ((y : Ordinal) → y o< x → odef X y → ⊥) ∨ choiced (& X)
                          lemma = ∀-imply-or lemma1
+                 odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< & X 
+                 odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {& X} ( c<→o< ( subst₂ (λ j k → odef j k )  (sym *iso) (sym &iso)  lt )) &iso &iso
                  have_to_find : choiced (& X)
                  have_to_find = dont-or  (lemma-ord (& X )) ¬¬X∋x where
                      ¬¬X∋x : ¬ ((x : Ordinal) → x o< (& X) → odef X x → ⊥)
                      ¬¬X∋x nn = not record {
-                            eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt) lt) 
+                            eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt)  lt) 
                           ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
                         }
 
@@ -154,7 +163,7 @@
               min2 : Minimal u
               min2 = prev (proj1 y1prop) u (proj2 y1prop)
          Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
-         Min2 x u u∋x = (ε-induction1 {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
+         Min2 x u u∋x = (ε-induction {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
          cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced (& x )
          cx {x} nx = choice-func x nx
          minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD 
diff -r 9984cdd88da3 -r cc7909f86841 OD.agda
--- a/OD.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/OD.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -13,9 +13,13 @@
 open import Relation.Binary.Core
 
 open import logic
+import OrdUtil
 open import nat
 
-open inOrdinal O
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal 
+open Ordinals.IsNext isNext 
+open OrdUtil O
 
 -- Ordinal Definable Set
 
@@ -258,12 +262,12 @@
     lemma : {z : Ordinal} → (z ≡ & x) ∨ (z ≡ & x) → & x ≡ z
     lemma (case1 refl) = refl
     lemma (case2 refl) = refl
-    y⊆x,x : {z : Ordinals.ord O} → def (od (x , x)) z → def (od y) z
+    y⊆x,x : {z : Ordinal} → def (od (x , x)) z → def (od y) z
     y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x 
     lemma1 : osuc (& y) o< & (x , x)
     lemma1 = subst (λ k → osuc (& y) o< k ) (sym (peq {x})) (osucc c ) 
 
-ε-induction : { ψ : HOD  → Set n}
+ε-induction : { ψ : HOD  → Set (suc n)}
    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
    → (x : HOD ) → ψ x
 ε-induction {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc )  where
@@ -272,16 +276,6 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy
 
--- level trick (what'a shame) for LEM / minimal
-ε-induction1 : { ψ : HOD  → Set (suc n)}
-   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
-   → (x : HOD ) → ψ x
-ε-induction1 {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc )  where
-     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox)
-     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) 
-     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
-     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (* oy)} induction oy
-
 Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
 Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
 
@@ -591,7 +585,7 @@
     ;   power→ = power→  
     ;   power← = power← 
     ;   extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} 
-    ;   ε-induction = ε-induction 
+    ;   ε-induction = ε-induction
     ;   infinity∅ = infinity∅
     ;   infinity = infinity
     ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
diff -r 9984cdd88da3 -r cc7909f86841 ODC.agda
--- a/ODC.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/ODC.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -12,15 +12,24 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
+import OrdUtil
 open import logic
 open import nat
 import OD
+import ODUtil
 
 open inOrdinal O
 open OD O
 open OD.OD
 open OD._==_
 open ODAxiom odAxiom
+open ODUtil O
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+
 
 open HOD
 
diff -r 9984cdd88da3 -r cc7909f86841 ODUtil.agda
--- a/ODUtil.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/ODUtil.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -15,8 +15,11 @@
 open import logic
 open import nat
 
-open inOrdinal O
-open import nat
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+import OrdUtil
+open OrdUtil O
 
 import OD
 open OD O
@@ -129,7 +132,7 @@
 ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → & y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
 
 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
-nat→ω-iso {i} = ε-induction1 {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
+nat→ω-iso {i} = ε-induction {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
      ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
                                             (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
      ind {x} prev lt = ind1 lt *iso where
diff -r 9984cdd88da3 -r cc7909f86841 OPair.agda
--- a/OPair.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/OPair.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -7,6 +7,8 @@
 open import zf
 open import logic
 import OD 
+import ODUtil
+import OrdUtil
 
 open import Relation.Nullary
 open import Relation.Binary
@@ -22,6 +24,13 @@
 open OD.HOD
 open ODAxiom odAxiom
 
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
+
 open _∧_
 open _∨_
 open Bool
diff -r 9984cdd88da3 -r cc7909f86841 Ordinals.agda
--- a/Ordinals.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/Ordinals.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -26,12 +26,10 @@
      <-osuc   : { x : ord  } → x o< osuc x
      osuc-≡<  : { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
      Oprev-p  : ( x : ord  ) → Dec ( Oprev ord osuc x )
-     TransFinite : { ψ : ord  → Set n }
+     TransFinite : { ψ : ord  → Set (suc n) }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
-     TransFinite1 : { ψ : ord  → Set (suc n) }
-          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
-          →  ∀ (x : ord)  → ψ x
+
 
 record IsNext {n : Level } (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
    field
@@ -51,5 +49,14 @@
 
 module inOrdinal  {n : Level} (O : Ordinals {n} ) where
 
-  open Ordinals O
-  open IsOrdinals 
+  open Ordinals  O
+  open IsOrdinals isOrdinal
+  open IsNext isNext
+
+  TransFinite0 : { ψ : Ordinal  → Set n }
+          → ( (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : Ordinal)  → ψ x
+  TransFinite0 {ψ} ind x = lower (TransFinite {λ y → Lift (suc n) ( ψ y)} ind1 x) where
+       ind1 : (z : Ordinal) → ((y : Ordinal) → y o< z → Lift (suc n) (ψ y)) → Lift (suc n) (ψ z)
+       ind1 z prev = lift (ind z (λ y y<z → lower (prev y y<z ) )) 
+
diff -r 9984cdd88da3 -r cc7909f86841 VL.agda
--- a/VL.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/VL.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -15,6 +15,14 @@
 import BAlgbra 
 open BAlgbra O
 open inOrdinal O
+import OrdUtil
+import ODUtil
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
 open OD O
 open OD.OD
 open ODAxiom odAxiom
@@ -30,7 +38,7 @@
 --    V α := ⋃ { V β | β < α }
 
 V : ( β : Ordinal ) → HOD
-V β = TransFinite1  V1 β where
+V β = TransFinite  V1 β where
    V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
    V1 x V0 with trio< x o∅
    V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
@@ -64,7 +72,7 @@
 --    V α := ⋃ { L β | β < α }
 
 L : ( β : Ordinal ) → Definitions → HOD
-L β D = TransFinite1  L1 β where
+L β D = TransFinite  L1 β where
    L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
    L1 x L0 with trio< x o∅
    L1 x L0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
diff -r 9984cdd88da3 -r cc7909f86841 cardinal.agda
--- a/cardinal.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/cardinal.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -21,6 +21,15 @@
 open OPair O
 open ODAxiom odAxiom
 
+import OrdUtil
+import ODUtil
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
+
 open _∧_
 open _∨_
 open Bool
diff -r 9984cdd88da3 -r cc7909f86841 filter.agda
--- a/filter.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/filter.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -19,6 +19,15 @@
 open OD.OD
 open ODAxiom odAxiom
 
+import OrdUtil
+import ODUtil
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
+
 import ODC
 open ODC O
 
diff -r 9984cdd88da3 -r cc7909f86841 generic-filter.agda
--- a/generic-filter.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/generic-filter.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -23,6 +23,14 @@
 open OD O
 open OD.OD
 open ODAxiom odAxiom
+import OrdUtil
+import ODUtil
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
 
 import ODC
 
diff -r 9984cdd88da3 -r cc7909f86841 ordinal.agda
--- a/ordinal.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/ordinal.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -10,6 +10,10 @@
 open import Relation.Nullary
 open import Relation.Binary.Core
 
+----
+--
+-- Countable Ordinals
+--
 
 data OrdinalD {n : Level} :  (lv : Nat) → Set n where
    Φ : (lv : Nat) → OrdinalD  lv
@@ -210,8 +214,7 @@
      ; ¬x<0 = ¬x<0 
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
-     ; TransFinite = TransFinite1
-     ; TransFinite1 = TransFinite2
+     ; TransFinite = TransFinite2
      ; Oprev-p  = Oprev-p 
    } ;
    isNext = record {
@@ -244,16 +247,6 @@
      Oprev-p  (ordinal lv (OSuc lv ox)) = yes record { oprev = ordinal lv ox ; oprev=x = refl }
      ord1 : Set (suc n)
      ord1 = Ordinal {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 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
-        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
-            ψ (record { lv = lx ; ord = OSuc lx x₁ })
-        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
      TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
           → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord1)  → ψ x
diff -r 9984cdd88da3 -r cc7909f86841 zf.agda
--- a/zf.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/zf.agda	Sat Aug 01 23:37:10 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 m}
+     ε-induction : { ψ : ZFSet → Set (suc m)}
               → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
               → (x : ZFSet ) → ψ x
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )