module set-of-agda where

open import Level

infix  50 _∧_

record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   constructor _×_
   field 
      proj1 : A
      proj2 : 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

infix  60 _∋_ _∈_

data _∋_   {n : Level} ( A : Set n ) : (a : A ) → Set n where
   elem :  (a : A) → A ∋ a

_∈_  : {n : Level} { A : Set n } →  (a : A ) →  Set n  → Set n
_∈_ {_} {A} a _  = A ∋ a

infix  40 _⇔_

_⇔_ : {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 )

-- 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 = {!!}