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