### changeset 424:cc7909f86841

remvoe TransFinifte1
author Shinji KONO Sat, 01 Aug 2020 23:37:10 +0900 9984cdd88da3 f7d66c84bc26 BAlgbra.agda LEMC.agda OD.agda ODC.agda ODUtil.agda OPair.agda Ordinals.agda VL.agda cardinal.agda filter.agda generic-filter.agda ordinal.agda zf.agda 13 files changed, 109 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
```--- 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```
```--- 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 ```
```--- 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}```
```--- 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
```
```--- 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```
```--- 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```
```--- 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 ) ))
+```
```--- 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)```
```--- 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```
```--- 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
```
```--- 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
```
```--- 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```
```--- 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 ) )```