1
------------------------------------------------------------------------
2
-- The Agda standard library
4
-- The irrelevance axiom
5
------------------------------------------------------------------------
7
module Irrelevance where
11
------------------------------------------------------------------------
12
-- The irrelevance axiom
14
-- There is no guarantee that this axiom is sound. Use it at your own
18
.irrelevance-axiom : ∀ {a} {A : Set a} → .A → A
20
{-# BUILTIN IRRAXIOM irrelevance-axiom #-}