------------------------------------------------------------------------
-- 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 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
-- Eta law for double-negation
¬¬-η : A → ¬ ¬ A
¬¬-η a ¬a = ¬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 ¬a = contradiction-irr a ¬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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4