module set-of-agda where

open import Level
open import Relation.Binary.HeterogeneousEquality

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 _∋_ _∈_

_∋_  : {n : Level} ( A : Set n ) → {a : A}  → { B : Set n} → ( b : B ) →  Set n
_∋_ A {a} {B} b = a ≅ b

_∈_  : {n : Level} { B : Set n } →  (b : B ) → ( A : Set n )  → {a : A}   →  Set n
_∈_ {_} {B} b A {a} = b ≅ 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 ) 
set-extentionality = {!!}