------------------------------------------------------------------------
-- 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  ¬_
¬_ : 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  _¬-⊎_
_¬-⊎_ : ¬ 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