--- a/set-of-agda.agda	Wed May 08 10:35:01 2019 +0900
+++ b/set-of-agda.agda	Wed May 08 11:34:23 2019 +0900
@@ -1,7 +1,6 @@
 module set-of-agda where
 
 open import Level
-open import Relation.Binary.HeterogeneousEquality
 
 infix  50 _∧_
 
@@ -21,11 +20,11 @@
 
 infix  60 _∋_ _∈_
 
-_∋_  : {n : Level} ( A : Set n ) → {a : A}  → { B : Set n} → ( b : B ) →  Set n
-_∋_ A {a} {B} b = a ≅ b
+data _∋_   {n : Level} ( A : Set n ) : (a : A ) → Set n where
+   elem :  (a : A) → A ∋ a
 
-_∈_  : {n : Level} { B : Set n } →  (b : B ) → ( A : Set n )  → {a : A}   →  Set n
-_∈_ {_} {B} b A {a} = b ≅ a
+_∈_  : {n : Level} { A : Set n } →  (a : A ) →  Set n  → Set n
+_∈_ {_} {A} a _  = A ∋ a
 
 infix  40 _⇔_
 
@@ -36,5 +35,29 @@
 -- ∀ 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 ) 
-set-extentionality = {!!}
+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
+
+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
+
+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
+
+-- set-regularity : {n : Level } → ( x : Set n) → ( ¬ ( x ⇔ ∅ ) ) → { y : x } → ( y ∩ x  ⇔ ∅ )
+-- set-regularity = {!!}
+