### changeset 274:29a85a427ed2

ε-induction
author Shinji KONO Sat, 25 Apr 2020 15:09:07 +0900 9ccf8514c323 455792eaa611 OD.agda cardinal.agda zf.agda 3 files changed, 12 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Sat Jan 11 20:11:51 2020 +0900
+++ b/OD.agda	Sat Apr 25 15:09:07 2020 +0900
@@ -316,14 +316,14 @@
;   power→ = power→
;   power← = power←
;   extensionality = λ {A} {B} {w} → extensionality {A} {B} {w}
-       -- ;   ε-induction = {!!}
+       ;   ε-induction = ε-induction
;   infinity∅ = infinity∅
;   infinity = infinity
;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
;   replacement← = replacement←
;   replacement→ = replacement→
-       ;   choice-func = choice-func
-       ;   choice = choice
+       -- ;   choice-func = choice-func
+       -- ;   choice = choice
} where

pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t == x ) ∨ ( t == y ) ```
```--- a/cardinal.agda	Sat Jan 11 20:11:51 2020 +0900
+++ b/cardinal.agda	Sat Apr 25 15:09:07 2020 +0900
@@ -5,6 +5,7 @@
open import zf
open import logic
import OD
+import OPair
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties
@@ -16,6 +17,7 @@
open inOrdinal O
open OD O
open OD.OD
+open OPair O

open _∧_
open _∨_```
```--- a/zf.agda	Sat Jan 11 20:11:51 2020 +0900
+++ b/zf.agda	Sat Apr 25 15:09:07 2020 +0900
@@ -19,7 +19,7 @@
(Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet )
(Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
(infinite : ZFSet)
-       : Set (suc (n ⊔ m)) where
+       : Set (suc (n ⊔ suc m)) where
field
isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
-- ∀ x ∀ y ∃ z ∀ t ( z ∋ t → t ≈ x ∨ t  ≈ y)
@@ -53,9 +53,9 @@
-- minimal : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet
-- regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimal x not  ∈ x ∧  (  minimal x not  ∩ x  ≈ ∅ ) )
-- another form of regularity
-     -- ε-induction : { ψ : ZFSet → Set m}
-     --         → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
-     --         → (x : ZFSet ) → ψ x
+     ε-induction : { ψ : ZFSet → Set (suc m)}
+              → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
+              → (x : ZFSet ) → ψ x
-- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
infinity∅ :  ∅ ∈ infinite
infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite
@@ -64,10 +64,10 @@
replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) → x ∈ X → ψ x ∈  Replace X ψ
replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )
-- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
-     choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
-     choice : (X : ZFSet  ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
+     -- choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
+     -- choice : (X : ZFSet  ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A

-record ZF {n m : Level } : Set (suc (n ⊔ m)) where
+record ZF {n m : Level } : Set (suc (n ⊔ suc m)) where
infixr  210 _,_
infixl  200 _∋_
infixr  220 _≈_```