module Lib.Zero where

open import Lib.Hide

data Zero : Set where

HideZero = Hide Zero

-- side note: the Agda stdlib currently implements Zero as Hide Zero
-- (https://agda.github.io/agda-stdlib/master/Data.Empty.html)
-- this way Agda can judgementally declare that all elements of ⊥ are equal
-- (especially functions that return a proof of ⊥ are equal)

magic : { A : Set } → Zero → A
magic ()