====== Agda ======

== Negation ==

The ''Negation'' definition in the [[https://agda.github.io/agda-stdlib/v2.0/Relation.Nullary.Negation.Core.html|stdlib]] is:
<code>
-- Negation.

infix 3 ¬_
¬_ : Set a → Set a
¬ A = A → ⊥

</code>

''A → ⊥ '' is the type of all functions from ''A'' to the empty type. You may have heard that you can prove anything from contradicting assumptions. So with this definition of ''¬ A'', if you assume ''A and ¬ A'', you can construct an element of the empty type, which lets you then prove anything. In fact, ⊥ is isomorphic to ''(X : Set) → X'', and an element of the second one is literally a proof of everything.