Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 274:29a85a427ed2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ε-induction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 Apr 2020 15:09:07 +0900
parents 9ccf8514c323
children 455792eaa611
files OD.agda cardinal.agda zf.agda
diffstat 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 _≈_