{-# 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
private
variable
a p q w : Level
A B C : Set a
Whatever : Set w
infix 3 ¬_
¬_ : Set a → Set a
¬ A = A → ⊥
DoubleNegation : Set a → Set a
DoubleNegation A = ¬ ¬ A
Stable : Set a → Set a
Stable A = ¬ ¬ A → A
infixr 1 _¬-⊎_
_¬-⊎_ : ¬ A → ¬ B → ¬ (A ⊎ B)
_¬-⊎_ = [_,_]
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
stable : ¬ ¬ Stable A
stable ¬[¬¬a→a] = ¬[¬¬a→a] (contradiction (¬[¬¬a→a] ∘ const))
negated-stable : Stable (¬ A)
negated-stable ¬¬¬a a = ¬¬¬a (contradiction a)
¬¬-map : (A → B) → ¬ ¬ A → ¬ ¬ B
¬¬-map f = contraposition (contraposition f)
private
note : (A → ¬ B) → B → ¬ A
note = flip