{-# OPTIONS --prop #-}
module zfctst where

data  : Prop where

data  : Prop where tt : 

data _∧_ (A : Prop) (B : Prop) : Prop where
  _and_ : A  B  A  B


π₁ : {A B : Prop}  (A  B)  A
π₁ (x and y) = x

π₂ : {A B : Prop}  (A  B)  B
π₂ (x and y) = y

data _∨_ (A : Prop) (B : Prop) : Prop where
  inj₁ : A  A  B
  inj₂ : B  A  B


data _≡_ {A : Set} (x : A) : A  Prop where
  refl : x  x

data pExists (A : Set) (B : A  Prop) : Prop  where
  pItExists : (a : A)  B a  pExists A B

data pExists' {A : Set} (B : A  Prop ) : Prop where
  pItExists : (a : A)  B a  pExists' {A = A} B


syntax pExists A  x  B) = ∃[ x of A ] B
syntax pExists'  x  B) = ∃[ x ] B

_↔_ : Prop  Prop  Prop
P  Q = (P  Q)  (Q  P)

mutual
  postulate
    ZFC : Set
    [_,_] : ZFC  ZFC  ZFC
    separate : (ZFC  Prop)  ZFC  ZFC
     : ZFC  ZFC
    𝓟 : ZFC  ZFC
     : ZFC
    ω : ZFC

  postulate
    _∈_ : ZFC  ZFC  Prop
  _⊆_ : ZFC  ZFC  Prop
  x  y = (z : ZFC)  z  x  z  y
  _~_ : ZFC  ZFC  Prop
  x ~ y = (x  y)  (y  x)
  data IsFunction (F : ZFC  ZFC  Prop) : Prop where
    itIsFunc : ((x y z : ZFC)  F x y  F x z  x ~ z)  IsFunction F
  postulate    pair-∈ : (x y z : ZFC)  (z  [ x , y ])  ((z ~ x)  (z ~ y))
               ∪-∈ : (x z : ZFC)  (∃[ y ] ((y  x)  (z  y)))  (z  ( x))
               ∅-∈ : (x : ZFC)  x    
  postulate replace : (F : ZFC  ZFC  Prop)  IsFunction F  ZFC  ZFC
  postulate replace-∈ : (F : ZFC  ZFC  Prop)  (p : IsFunction F)  (X : ZFC)  ((y : ZFC)  (y  replace F p X)  ((∃[ x ] ((x  X)  (F x y)))))
  postulate separate-∈ : (P : ZFC  Prop)  (X : ZFC)  (u : ZFC)  (u  separate P X)  ((u  X)  P u)
  postulate 𝓟-∈ : (x y : ZFC)  (y  x)  (y  (𝓟 x))
  postulate ext : (x y : ZFC)  (x ~ y)  (x  y)
  postulate ω₁-∈ :   ω
  postulate ω₂-∈ : (x : ZFC)  x  ω  ( [ [ x , x ] , x ])  ω

[_] : ZFC  ZFC
[ x ] = [ x , x ]

∨-elim : {A B C : Prop}  (A  C)  (B  C)  (A  B)  C
∨-elim f g (inj₁ x) = f x
∨-elim f g (inj₂ x) = g x

[_]-singleton : (x y : ZFC)  y  [ x , x ]  y ~ x
[ x ]-singleton y p =  z q  ∨-elim  eq  π₁ eq z q)  eq  π₁ eq z q) (π₁ (pair-∈ x x y) p)) and
   z q  ∨-elim  x₁  π₂ x₁ z q)  x₁  π₂ x₁ z q) (π₁ (pair-∈ x x y) p))

[_,_]-swap : (x y : ZFC)  [ x , y ] ~ [ y , x ]
[ x , y ]-swap = helper and helper2
  where helper :  {x} {y} z  z  [ x , y ]  z  [ y , x ]
        helper z p = ∨-elim  x  π₂ (pair-∈ _ _ _) (inj₂ x)) ((λ x  π₂ (pair-∈ _ _ _) (inj₁ x))) (π₁ (pair-∈ _ _ _) p)
        helper2 :  {x} {y} z  z  [ y , x ]  z  [ x , y ]
        helper2 z p = ∨-elim  x  π₂ (pair-∈ _ _ _) (inj₂ x)) ((λ x  π₂ (pair-∈ _ _ _) (inj₁ x))) (π₁ (pair-∈ _ _ _) p)

⦅_,_⦆ : ZFC  ZFC  ZFC
 x , y  = [ [ x ] , [ x , y ] ]

-- will prove when needed...
-- ⦅_,_⦆-eq : (x y : ZFC) → (a b : ZFC) → ((⦅ x , y ⦆) ~ (⦅ a , b ⦆)) ↔ ((x ~ a) ∧ (y ~ b))
-- ⦅ x , y ⦆-eq a b = 

_∩_ _-_ : ZFC  ZFC  ZFC
X  Y = separate  x  x  Y) X

_∉_ : ZFC  ZFC  Prop
x  y = x  y  

X - Y = separate  x  x  Y) X

_and_are-disjoint : ZFC  ZFC  Prop
X and Y are-disjoint = (X  Y) ~ 

 : (X x : ZFC)  x  X  ZFC
 X x p = separate  y  (Y : ZFC)  (Y  X)  y  Y) x

_∪_ : ZFC  ZFC  ZFC
x  y =  [ x , y ]