The Negation definition in the stdlib is:

-- Negation.

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

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.