no good

set.agda

module Set-Syntax where
  Σ-syntax′ : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
  Σ-syntax′ = Σ

  syntax Σ-syntax′ A (\x → B) = [ x ∈ A ∣ B ]

  Σ-type : ∀{a b} → Set a → Set b → Set _
  Σ-type A B = Σ A (\_ → B)

  syntax Σ-type A P = P ⊆ A

--  ∅ : {A : Set} → A → Set
--  ∅ = \_ → ⊥

--  U₀ : {A : Set} → A → Set
--  U₀ = \_ → ⊤

  ¬ : Set → Set
  ¬ P = P → ⊥

  singleton : {A : Set} → (x : A) → Set
  singleton {A = A} x = [ y ∈ A ∣ y ≡ x ]

  isSingleton : (A : Set) → Set
  isSingleton A = [ y ∈ A ∣ (∀(x : A) → x ≡ y) ]

  singleton-isSingleton : {A : Set} (x : A) → isSingleton (singleton x)
  singleton-isSingleton x = ((x , refl) , \{(.x , refl) → refl})

  In : Set → Set → Set
  In A z = isSingleton z × z ⊆ A

  syntax In A z = z ∈ A

  NotIn : Set → Set → Set
  NotIn A z = ¬ (z ∈ A)

  syntax NotIn A z = z ∉ A

open Set-Syntax public

singleton-⊆ : (A : Set) → (x : A) → singleton x ⊆ A
singleton-⊆ A x = x , (x , refl)

elem-∈ : (A : Set) → (x : A) → singleton x ∈ A
elem-∈ A x = x , (singleton-isSingleton x , (x , refl))

--∅-⊆ : (A : Set) → ⊥ ⊆ A
--∅-⊆ A = {!!} , {!!}

infix 3 _⇔_
_⇔_ : (A B : Set) → Set
A ⇔ B = A → B × B → A

_∩_ : (A B : Set) → Set₁
A ∩ B = ∃ \x → (x ∈ A) × (x ∈ B)

module Axioms where
--  AxiomOfExtensionality : Set₁

  AxiomOfChoice : Set₁
  AxiomOfChoice = {A B : Set} {R : A → B → Set}
    → (∀ (a : A) → ∃ (\(b : B) → R a b))
    → (∃ \(f : A → B) → ∀ (a : A) → R a (f a))

  ac : AxiomOfChoice
  ac h = proj₁ ∘ h , proj₂ ∘ h