Type theory
Home
Table of Contents
1. The Curry-Howard Isomorphism
| Type theory | Set theory | Logic |
|---|---|---|
| A : Type | set | proposition |
| a : A | element | proof |
| A → B | set of functions | implication |
| A × B | cartesian product | conjunction |
| A + B | disjoint union | disjunction |
| unit | singleton | ⊤ |
| empty | ∅ | ⊥ |
| x:A ⊢ B(x):Type | {Bx}x ∈ A | predicate |
| x:A ⊢ b(x):B(x) | family of elements | conditional proof |
| Σ (x:A), B(x) | ⊔x ∈ A Bx | ∃ (x : A), B(x) |
| Π (x:A), B(x) | Πx ∈ A Bx | ∀ (x : A), B(x) |