    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Core properties related to negation
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Relation.Nullary.Negation.Core where

    open import Data.Empty using (⊥; ⊥-elim-irr)
    open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
    open import Function.Base using (flip; _∘_; const)
    open import Level using (Level; _⊔_)

    private
      variable
        a p q w : Level
        A B C : Set a
        Whatever : Set w

    ------------------------------------------------------------------------
    -- Negation.

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

    ------------------------------------------------------------------------
    -- Stability.

    -- Double-negation
    DoubleNegation : Set a → Set a
    DoubleNegation A = ¬ ¬ A

    -- Stability under double-negation.
    Stable : Set a → Set a
    Stable A = ¬ ¬ A → A

    ------------------------------------------------------------------------
    -- Relationship to sum

    infixr 1 _¬-⊎_
    _¬-⊎_ : ¬ A → ¬ B → ¬ (A ⊎ B)
    _¬-⊎_ = [_,_]

    ------------------------------------------------------------------------
    -- Uses of negation

    contradiction-irr : .A → ¬ A → Whatever
    contradiction-irr a ¬a = ⊥-elim-irr (¬a a)

    contradiction : A → ¬ A → Whatever
    contradiction a = contradiction-irr a

    contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
    contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a
    contradiction₂ (inj₂ b) ¬a ¬b = contradiction b ¬b

    contraposition : (A → B) → ¬ B → ¬ A
    contraposition f ¬b a = contradiction (f a) ¬b

    -- Self-contradictory propositions are false by 'diagonalisation'

    contra-diagonal : (A → ¬ A) → ¬ A
    contra-diagonal self a = self a a

    -- Everything is stable in the double-negation monad.
    stable : ¬ ¬ Stable A
    stable ¬[¬¬a→a] = ¬[¬¬a→a] (contradiction (¬[¬¬a→a] ∘ const))

    -- Negated predicates are stable.
    negated-stable : Stable (¬ A)
    negated-stable ¬¬¬a a = ¬¬¬a (contradiction a)

    ¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B
    ¬¬-map f = contraposition (contraposition f)

    -- Note also the following use of flip:
    private
      note : (A → ¬ B) → B → ¬ A
      note = flip