Calculus of inductive constructions

Remarks

Example: the natural numbers are the inductive type $\mathsf{nat} : \mathsf{Type}_0$ with $\mathsf{O} : \mathsf{nat}$ and $\mathsf{S} : \mathsf{nat} \to \mathsf{nat}$. Addition is the fixed point with $\mathsf{plus}\ \mathsf{O}\ m = m$ and $\mathsf{plus}\ (\mathsf{S}\, n)\ m = \mathsf{S}\,(\mathsf{plus}\ n\ m)$, which is accepted because the recursive call is on the smaller argument $n$.

Non-example: the judgment $\mathsf{Type}_0 : \mathsf{Type}_0$ is not derivable; the universe $\mathsf{Type}_i$ only has type $\mathsf{Type}_{i+1}$. A type of all types would make the system inconsistent by Girard's paradox.

Equality is itself an inductive family: for $A$ a type and $a : A$, the family $\mathsf{eq}\ A\ a$ over $A$ has the single constructor $\mathsf{eq\_refl} : \mathsf{eq}\ A\ a\ a$, a case of a dependent type defined inductively. In the system used by Coq the universes are cumulative: a type in $\mathsf{Type}_i$ also lies in $\mathsf{Type}_{i+1}$. Eliminations from inductive types in $\mathsf{Prop}$ into other sorts are restricted, to keep proofs irrelevant to computation.