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

module Irrelevance where

import Level

------------------------------------------------------------------------
-- The irrelevance axiom

-- There is no guarantee that this axiom is sound. Use it at your own
-- risk.

postulate
  .irrelevance-axiom : ∀ {a} {A : Set a} → .A → A

{-# BUILTIN IRRAXIOM irrelevance-axiom #-}