# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1557331159 -32400
# Node ID 5c819f8377215cd23097512313cb8705a8754c08
# Parent  a63df8c7711465f2916e048a03345151010727d8
...

diff -r a63df8c77114 -r 5c819f837721 set-of-agda.agda
--- a/set-of-agda.agda	Wed May 08 11:34:23 2019 +0900
+++ b/set-of-agda.agda	Thu May 09 00:59:19 2019 +0900
@@ -1,63 +1,104 @@
 module set-of-agda where
 
 open import Level
+open import Data.Bool
 
-infix  50 _∧_
+-- infix  50 _∧_
+
+-- record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+--    constructor _×_
+--    field 
+--       proj1 : A
+--       proj2 : B
+
+-- open _∧_
 
-record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
-   constructor _×_
-   field 
-      proj1 : A
-      proj2 : B
+-- infix  50 _∨_
+
+-- data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+--    case1 : A → A ∨ B
+--    case2 : B → A ∨ B
 
-open _∧_
-
-infix  50 _∨_
-
-data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
-   case1 : A → A ∨ B
-   case2 : B → A ∨ B
+data ZFSet {n : Level} : Set (suc n) where
+    elem : { A : Set  n } ( a : A ) → ZFSet 
+    ∅ : ZFSet  {n}
+    pair : {A B : Set n} (a : A ) (b : B ) → ZFSet 
+    union :  (A  : ZFSet {n}) → ZFSet  
+    repl :  { A B : Set n}  → ( ψ : A → B )  → ZFSet 
+    infinite : ZFSet 
+    power : (A  : ZFSet {n})  → ZFSet 
 
 infix  60 _∋_ _∈_
 
-data _∋_   {n : Level} ( A : Set n ) : (a : A ) → Set n where
-   elem :  (a : A) → A ∋ a
+open import Relation.Binary.PropositionalEquality 
 
-_∈_  : {n : Level} { A : Set n } →  (a : A ) →  Set n  → Set n
-_∈_ {_} {A} a _  = A ∋ a
+data _∈_ {n : Level} : {A : Set n}  ( a : A )  ( Z : ZFSet {n} )  → Set (suc n) where
+    ∈-elm : {A : Set n } {a : A} →  a ∈ (elem a)   
+    ∈-pair-1 : {A : Set n } {B : Set n} {b : B} {a : A}  → a ∈  (pair a b)   
+    ∈-pair-2 : {A : Set n } {B : Set n} {b : A} {a : B}  → b ∈  (pair a b)   
+--    ∈-union : {Z : ZFSet {n}} {A : Set n}  → { b : ZFSet {n} } → {!!}  → a ∈ (union Z)  
+    ∈-repl : {A : Set n } { B : Set n}  → { ψ : B → A } → { b : B } → ψ b ∈  (repl ψ) 
+    -- ∈-infinite-1 : ∅ ∈ infinite 
+--    ∈-infinite : {A : Set n} {a : A} → _∈_  infinite {A} a 
+    ∈-power : {A : Set n} {Z : ZFSet {n}} {a : A → B } → a ∈  (power Z)  
+
+-- _∈_  : {n : Level} { A : ZFSet {n} } → {B : Set n} →  (a : B ) →  Set n  → Bool
+-- _∈_ {_} {A} a _  = A ∋ a
 
 infix  40 _⇔_
 
-_⇔_ : {n : Level} (A  B : Set n)  → Set  n 
-A ⇔ B = ( ∀ {x : A } → x ∈ B  ) ∧  ( ∀ {x : B } → x ∈ A )
+-- _⇔_ : {n : Level} (A  B : Set n)  → Set  n 
+-- A ⇔ B = ( ∀ {x : A } → x ∈ B  ) ∧  ( ∀ {x : B } → x ∈ A )
 
 -- Axiom of extentionality
 -- ∀ x ∀ y [ ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) ]
 
-set-extentionality : {n : Level } {x y : Set n }  → { z : x } → ( z ∈ x ⇔ z ∈ y ) → ∀ (w : Set (suc n))  → ( x ∈ w ⇔ y ∈ w ) 
-proj1 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .x} = elem ( elem x )
-proj2 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .y} = elem ( elem y )
+-- set-extentionality : {n : Level } {x y : Set n }  → { z : x } → ( z ∈ x ⇔ z ∈ y ) → ∀ (w : Set (suc n))  → ( x ∈ w ⇔ y ∈ w ) 
+-- proj1 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .x} = elem ( elem x )
+-- proj2 (set-extentionality {n} {x} {y} {z} (z∈x→z∈y × z∈x←z∈y) w) {elem .y} = elem ( elem y )
 
--- Axiom of regularity 
--- ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
 
 open import Relation.Nullary
 open import Data.Empty
 
-data ∅  : Set where
+-- data ∅  : Set where
 
 infix  50 _∩_
 
-record _∩_ {n m : Level} (A : Set n) ( B : Set m)  : Set (n ⊔ m) where
-   field
-      inL : {x : A } → x ∈ A
-      inR : {x : B } → x ∈ B
+-- record _∩_ {n m : Level} (A : Set n) ( B : Set m)  : Set (n ⊔ m) where
+--    field
+--       inL : {x : A } → x ∈ A
+--       inR : {x : B } → x ∈ B
 
-open _∩_
+-- open _∩_
 
 -- lemma : {n m : Level} (A : Set n) ( B : Set m) → (a : A ) → a ∈ (A ∩ B) 
 -- lemma A B a A∩B = inL A∩B
 
+-- Axiom of regularity 
+-- ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
+
 -- set-regularity : {n : Level } → ( x : Set n) → ( ¬ ( x ⇔ ∅ ) ) → { y : x } → ( y ∩ x  ⇔ ∅ )
 -- set-regularity = {!!}
 
+--  Axiom of pairing
+-- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z).
+
+-- pair : {n m : Level}  ( x : Set n ) ( y : Set m ) → Set (n ⊔ m)
+-- pair x y = {!!} -- ( x × y )
+
+-- Axiom of Union
+-- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t  ∈ x))
+
+-- axiom of infinity
+-- ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
+
+-- axiom of replacement
+-- ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
+
+-- axiom of power set
+-- ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) ) 
+
+
+
+