This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Negation

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

open import foundation-core.empty-types

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.

Definition

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)