Negation

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

Created on 2022-03-05.
Last modified on 2026-05-02.

module foundation-core.negation where
Imports 
open import foundation.universe-levels

open import foundation-core.empty-types
open import foundation-core.logical-equivalences

Idea

The Curry–Howard interpretation of negation in type theory is the interpretation of the proposition P ⇒ ⊥ using propositions as types. Thus, the negation of a type A is the type A → empty.

Definitions

infix 25 ¬_

¬_ : {l : Level} → UU l → UU l
¬ A = A → empty

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

Reductio ad absurdum

reductio-ad-absurdum : {l1 l2 : Level} {P : UU l1} {Q : UU l2} → P → ¬ P → Q
reductio-ad-absurdum p np = ex-falso (np p)

Negation has no fixed points

no-fixed-points-neg :
  {l : Level} (A : UU l) → ¬ (A ↔ ¬ A)
no-fixed-points-neg A e =
  ( λ (h : ¬ A) → h (backward-implication e h))
  ( λ (a : A) → forward-implication e a a)

Recent changes