module Empty where

open import Equality
open import FunctionExtensionality
open import Level

data Ø {ℓ : Level} : Set ℓ where

Ø-elim :
  {ℓ ℓ' : Level}
  {A : Set ℓ'}
  → -----------
  Ø {ℓ} → A
Ø-elim ()

ØisProp :
  {ℓ : Level}
  {x y : Ø {ℓ}}
  → -----------
  x ≡ y
ØisProp {x = ()}

Øuniq :
  {ℓ ℓ' : Level}
  {A : Set ℓ'}
  (f g : Ø {ℓ} → A)
  → ---------------
  f ≡ g
Øuniq f g = funext (λ ())