# Double negation

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-01-27.

module foundation.double-negation where

Imports
open import foundation.dependent-pair-types
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.coproduct-types
open import foundation-core.empty-types
open import foundation-core.function-types
open import foundation-core.propositions


## Definition

We define double negation and triple negation

¬¬ : {l : Level} → UU l → UU l
¬¬ P = ¬ (¬ P)

¬¬¬ : {l : Level} → UU l → UU l
¬¬¬ P = ¬ (¬ (¬ P))


We also define the introduction rule for double negation, and the action on maps of double negation.

intro-double-negation : {l : Level} {P : UU l} → P → ¬¬ P
intro-double-negation p f = f p

map-double-negation :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} → (P → Q) → (¬¬ P → ¬¬ Q)
map-double-negation f = map-neg (map-neg f)


## Properties

### The double negation of a type is a proposition

double-negation-Prop' :
{l : Level} (A : UU l) → Prop l
double-negation-Prop' A = neg-Prop' (¬ A)

double-negation-Prop :
{l : Level} (P : Prop l) → Prop l
double-negation-Prop P = double-negation-Prop' (type-Prop P)

is-prop-double-negation :
{l : Level} {A : UU l} → is-prop (¬¬ A)
is-prop-double-negation = is-prop-neg


### Double negations of classical laws

double-negation-double-negation-elim :
{l : Level} {P : UU l} → ¬¬ (¬¬ P → P)
double-negation-double-negation-elim {P = P} f =
( λ (np : ¬ P) → f (λ (nnp : ¬¬ P) → ex-falso (nnp np)))
( λ (p : P) → f (λ (nnp : ¬¬ P) → p))

double-negation-Peirces-law :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} → ¬¬ (((P → Q) → P) → P)
double-negation-Peirces-law {P = P} f =
( λ (np : ¬ P) → f (λ h → h (λ p → ex-falso (np p))))
( λ (p : P) → f (λ _ → p))

double-negation-linearity-implication :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} →
¬¬ ((P → Q) + (Q → P))
double-negation-linearity-implication {P = P} {Q = Q} f =
( λ (np : ¬ P) →
map-neg (inl {A = P → Q} {B = Q → P}) f (λ p → ex-falso (np p)))
( λ (p : P) → map-neg (inr {A = P → Q} {B = Q → P}) f (λ _ → p))


### Cases of double negation elimination

double-negation-elim-neg : {l : Level} (P : UU l) → ¬¬¬ P → ¬ P
double-negation-elim-neg P f p = f (λ g → g p)

double-negation-elim-prod :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} →
¬¬ ((¬¬ P) × (¬¬ Q)) → (¬¬ P) × (¬¬ Q)
pr1 (double-negation-elim-prod {P = P} {Q = Q} f) =
double-negation-elim-neg (¬ P) (map-double-negation pr1 f)
pr2 (double-negation-elim-prod {P = P} {Q = Q} f) =
double-negation-elim-neg (¬ Q) (map-double-negation pr2 f)

double-negation-elim-exp :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} →
¬¬ (P → ¬¬ Q) → (P → ¬¬ Q)
double-negation-elim-exp {P = P} {Q = Q} f p =
double-negation-elim-neg
( ¬ Q)
( map-double-negation (λ (g : P → ¬¬ Q) → g p) f)

double-negation-elim-forall :
{l1 l2 : Level} {P : UU l1} {Q : P → UU l2} →
¬¬ ((p : P) → ¬¬ (Q p)) → (p : P) → ¬¬ (Q p)
double-negation-elim-forall {P = P} {Q = Q} f p =
double-negation-elim-neg
( ¬ (Q p))
( map-double-negation (λ (g : (u : P) → ¬¬ (Q u)) → g p) f)


### Maps into double negations extend along intro-double-negation

double-negation-extend :
{l1 l2 : Level} {P : UU l1} {Q : UU l2} →
(P → ¬¬ Q) → (¬¬ P → ¬¬ Q)
double-negation-extend {P = P} {Q = Q} f =
double-negation-elim-neg (¬ Q) ∘ (map-double-negation f)


### The double negation of a type is logically equivalent to the double negation of its propositional truncation

abstract
double-negation-double-negation-type-trunc-Prop :
{l : Level} (A : UU l) → ¬¬ (type-trunc-Prop A) → ¬¬ A
double-negation-double-negation-type-trunc-Prop A =
double-negation-extend
( map-universal-property-trunc-Prop
( double-negation-Prop' A)
( intro-double-negation))

abstract
double-negation-type-trunc-Prop-double-negation :
{l : Level} {A : UU l} → ¬¬ A → ¬¬ (type-trunc-Prop A)
double-negation-type-trunc-Prop-double-negation =
map-double-negation unit-trunc-Prop