module set-of-agda where

open import Level
open import Data.Bool

-- 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

data ZFSet {n : Level} : Set (suc (suc n)) where
    elem : { A : Set  n } ( a : A ) → ZFSet 
    ∅ : ZFSet  {n}
    pair : {A B : Set n} (a : A ) (b : B ) → ZFSet 
    union :  (A  : Set (suc n) ) → ZFSet  
    -- repl :  ( ψ : ZFSet {n} →  Set zero )   → ZFSet 
    infinite : ZFSet 
    power : (A  : ZFSet {n})  → ZFSet 

infix  60 _∋_ _∈_

open import Relation.Binary.PropositionalEquality 

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 : Set (suc n)}  {A : Z }  → {a : {!!} } → 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 B : 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 )

-- 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 )


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

-- 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 ) )