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

changeset 7:813f1b3b000b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 May 2019 19:14:16 +0900
parents d9b704508281
children cb014a103467
files zf.agda
diffstat 1 files changed, 43 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/zf.agda	Sat May 11 11:40:31 2019 +0900
+++ b/zf.agda	Sat May 11 19:14:16 2019 +0900
@@ -50,7 +50,7 @@
      union← : ( X x y : ZFSet  ) → Union X  ∋ y → X ∋ x  → x ∋ y 
   _∈_ : ( A B : ZFSet  ) → Set m
   A ∈ B = B ∋ A
-  _⊆_ : ( A B : ZFSet  ) → { x : ZFSet } → { A∋x : Set m } → Set m
+  _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } → ∀{ A∋x : Set m } → Set m
   _⊆_ A B {x} {A∋x} = B ∋ x
   _∩_ : ( A B : ZFSet  ) → ZFSet
   A ∩ B = Restrict ( λ x → ( A ∋ x ) ∧ ( B ∋ x ) )
@@ -67,8 +67,8 @@
      -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extentionality :  ( A B z  : ZFSet  ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
      -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
-     -- smaller : ZFSet → ZFSet
-     -- regularity : ( x : ZFSet  ) → ¬ (x ≈ ∅) → smaller x  ∩ x  ≈ ∅ 
+     smaller : ZFSet → ZFSet
+     regularity : ( x : ZFSet  ) → ¬ (x ≈ ∅) → smaller x  ∩ x  ≈ ∅ 
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ( x : ZFSet  ) → x ∈ infinite →  ( x ∪ Restrict ( λ y → x ≈ y )) ∈ infinite 
@@ -91,6 +91,45 @@
      Power : ( A : ZFSet  ) → ZFSet
      Restrict : ( ZFSet → Set m ) → ZFSet
      infinite : ZFSet
-  field
      isZF : IsZF ZFSet _∋_ _≈_ ∅ _×_ Union Power Restrict infinite 
 
+module reguraliry-m {n m : Level } ( zf : ZF {m} {n} ) where
+
+   open import Relation.Nullary
+   open import Data.Empty
+   open import  Relation.Binary.PropositionalEquality
+
+   _≈_ =  ZF._≈_ zf
+   ZFSet =  ZF.ZFSet 
+   Restrict =  ZF.Restrict  zf
+   ∅ =  ZF.∅ zf
+   _∩_ =  ( IsZF._∩_  ) (ZF.isZF zf)
+   _∋_ =   ZF._∋_  zf
+   replacement =   IsZF.replacement  ( ZF.isZF zf )
+
+   russel : ( x : ZFSet zf ) → x ≈ Restrict ( λ x → ¬ ( x ∋ x ) ) → ⊥
+   russel x eq with  x ∋ x 
+   ... | x∋x  with replacement ( λ x → ¬ ( x ∋ x )) x {!!}
+   ... | r1 = {!!}
+
+
+
+
+data Nat : Set zero where
+  Zero : Nat
+  Suc : Nat → Nat
+
+prev : Nat → Nat
+prev (Suc n) = n
+prev Zero = Zero
+
+open import  Relation.Binary.PropositionalEquality
+
+
+-- data Transtive {n : Level } ( lv : Nat) : Set n where
+--   Φ : lv ≡ Zero → Transtive lv
+--   pair : (s : Transtive (prev lv) ) → (t : Transtive (prev lv) ) → Transtive lv
+
+
+
+