Calculus of constructions

Definition

The calculus of constructions is the pure type system with two sorts $*$ (also written $\mathsf{Prop}$) and $\square$ (also written $\mathsf{Type}$), given as follows. The terms are $t ::= x \mid * \mid \square \mid t\, t \mid \lambda x{:}t.\, t \mid \Pi x{:}t.\, t$. The typing relation $\Gamma \vdash t : T$ is the least relation closed under these rules, where $s, s_1, s_2$ range over $\set{*, \square}$.

1. Axiom: $\vdash * : \square$.
2. Start and weakening: if $\Gamma \vdash A : s$ and $x$ is a fresh variable, then $\Gamma, x : A \vdash x : A$, and every judgment of $\Gamma$ also holds in $\Gamma, x : A$.
3. Product: if $\Gamma \vdash A : s_1$ and $\Gamma, x : A \vdash B : s_2$, then $\Gamma \vdash \Pi x{:}A.\, B : s_2$, for each of the four pairs $(s_1, s_2)$.
4. Abstraction: if $\Gamma, x : A \vdash b : B$ and $\Gamma \vdash \Pi x{:}A.\, B : s$, then $\Gamma \vdash \lambda x{:}A.\, b : \Pi x{:}A.\, B$.
5. Application: if $\Gamma \vdash f : \Pi x{:}A.\, B$ and $\Gamma \vdash a : A$, then $\Gamma \vdash f\, a : B[a/x]$.
6. Conversion: if $\Gamma \vdash t : A$, $\Gamma \vdash B : s$ and $A$ and $B$ are equal up to beta reduction, then $\Gamma \vdash t : B$.