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

Created on 2022-03-05.
Last modified on 2024-04-11.

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

open import foundation-core.empty-types


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.


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)

Recent changes