Martin Escardo. Notes originally written for the module Advanced Functional Programming of the University of Birmingham, UK.
{-# OPTIONS --without-K #-}
module curry-howard whereWe now complete the proposition-as-types interpretation of logic.
| Logic | English | Type theory | Agda | Handouts | Alternative terminology |
|---|---|---|---|---|---|
| ⊥ | false | ℕ₀ | 𝟘 | empty type | |
| ⊤ | true (*) | ℕ₁ | 𝟙 | unit type | |
| A ∧ B | A and B | A × B | A × B | binary product | cartesian product |
| A ∨ B | A or B | A + B | A ∔ B | binary sum | coproduct, binary disjoint union |
| A → B | A implies B | A → B | A → B | function type | non-dependent function type |
| ¬ A | not A | A → ℕ₀ | A → 𝟘 | negation | |
| ∀ x : A, B x | for all x:A, B x | Π x : A , B x | (x : A) → B x | product | dependent function type |
| ∃ x : A, B x | there is x:A such that B x | Σ x ꞉ A , B x | Σ x ꞉ A , B x | sum | disjoint union, dependent pair type |
| x = y | x equals y | Id x y | x ≡ y | identity type | equality type, propositional equality |
-
(*) Not only the unit type 𝟙, but also any type with at least one element can be regarded as "true" in the propositions-as-types interpretation.
-
In Agda we can use any notation we like, of course, and people do use slightly different notatations for e.g.
𝟘,𝟏,+andΣ. -
We will refer to the above type theory together with the type
ℕof natural numbers as Basic Martin-Löf Type Theory. -
As we will see, this type theory is very expressive and allows us to construct rather sophisticated types, including e.g. lists, vectors and trees.
-
All types in MLTT (Martin-Löf type theory) come with introduction and elimination principles.