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)

Author: Vaibhav Karve

Created: 2021-04-08 Thu 10:50

Validate