There is exactly one way to choose 0 elements from the empty set.

Choose.agda

module Choose where

open import Data.Product using (_,_ ; proj₁ ; proj₂ ; ∃) renaming (_×_ to _∧_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; sym ; subst)
open import Relation.Nullary using (¬_)

infix 0 _⇔_
_⇔_ : Set → Set → Set
A ⇔ B = (A → B) ∧ (B → A)

postulate
  set : Set
  _∈_ : set → set → Set

_⊆_ : set → set → Set
a ⊆ b = ∀ x → x ∈ a → x ∈ b

postulate
  ZF-extensionality : ∀ {x y} → (∀ z → z ∈ x ⇔ z ∈ y) → x ≡ y
  ZF-specification : ∀ (P : set → Set) z → ∃ (λ y → ∀ x → x ∈ y ⇔ x ∈ z ∧ P x)
  ZF-pairing : ∀ x y → ∃ (λ z → x ∈ z ∧ y ∈ z)
  ZF-powerset : ∀ x → ∃ (λ y → ∀ z → z ⊆ x → z ∈ y)
  ZF-emptyset : ∃ (λ x → ∀ y → ¬ y ∈ x)

proper-powerset : ∀ x → ∃ (λ y → ∀ z → z ⊆ x ⇔ z ∈ y)
proper-powerset x =
  let px , f = ZF-powerset x in
  let ppx , g = ZF-specification (_⊆ x) px in
  ppx , λ y →
    (λ y⊆x → proj₂ (g y) (f y y⊆x , y⊆x)) ,
    (λ y∈ppx → proj₂ (proj₁ (g y) y∈ppx))

subsets-of : set → set
subsets-of x = proj₁ (proper-powerset x)

specified : (set → Set) → set → set
specified P x = proj₁ (ZF-specification P x)

Empty : set
Empty = proj₁ ZF-emptyset

Zero : set
Zero = Empty

one : ∃ (λ One → ∀ z → z ∈ One ⇔ z ≡ Zero)
one =
  let pzz , a , b = ZF-pairing Zero Zero in
  let One , g = ZF-specification (_≡ Zero) pzz in
  One , λ z →
    (λ z∈1 → proj₂ (proj₁ (g z) z∈1)) ,
    (λ z≡0 → proj₂ (g z) (subst (_∈ _) (sym z≡0) a , z≡0))

One : set
One = proj₁ one

lem₁ : ∀ {z} → z ≡ Empty → z ⊆ Empty
lem₁ z≡0 x x∈z = subst (x ∈_) z≡0 x∈z

lem₂ : ∀ {z} → z ≡ Empty → z ∈ subsets-of Empty
lem₂ {z} z≡0 = proj₁ (proj₂ (proper-powerset Empty) z) (lem₁ z≡0)

thm : specified (_≡ Zero) (subsets-of Empty) ≡ One
thm =
  let h1 = proj₂ (ZF-specification (_≡ Zero) (subsets-of Empty)) in
  ZF-extensionality λ z →
    (λ z∈s →
      let z≡0 = proj₂ (proj₁ (h1 z) z∈s) in
      proj₂ (proj₂ one z) z≡0) ,
    (λ z∈1 →
      let z≡0 = proj₁ (proj₂ one z) z∈1 in
      proj₂ (h1 z) (lem₂ z≡0 , z≡0))