Martin Escardo. Notes originally written for the module Advanced Functional Programming of the University of Birmingham, UK.
{-# OPTIONS --without-K #-} module curry-howard where
Propositions as types and basic Martin-Löf type theory
We 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 |
Remarks
(*) 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.