------------------------------------------------------------------------ -- 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