# 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 | {B_{x}}_{x ∈ A} |
predicate |

x:A ⊢ b(x):B(x) | family of elements | conditional proof |

Σ (x:A), B(x) | ⊔_{x ∈ A} B_{x} |
∃ (x : A), B(x) |

Π (x:A), B(x) | Π_{x ∈ A} B_{x} |
∀ (x : A), B(x) |