Negation
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-03-05.
Last modified on 2023-06-08.
module foundation-core.negation where
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
¬ : {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
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).