------------------------------------------------------------------------
-- The Agda standard library
--
-- The irrelevance axiom
------------------------------------------------------------------------

module Irrelevance where

import Level