Inductive type

Remarks

Example: the natural numbers are the inductive type $\N$ with constructors $\mathsf{zero} : \N$ and $\mathsf{succ} : \N \to \N$. Strict positivity holds, since the only argument of $\mathsf{succ}$ is $\N$ itself. Rule 3 is the induction principle: to give $f : \Pi_{n : \N} P(n)$ one gives $f(\mathsf{zero}) : P(\mathsf{zero})$ and, for each $n$, $f(\mathsf{succ}\, n) : P(\mathsf{succ}\, n)$ computed from $n$ and $f(n)$.

Non-example: a type $D$ with one constructor $\mathsf{lam} : (D \to D) \to D$ is rejected. The argument type $D \to D$ mentions $D$ to the left of an arrow, so strict positivity fails. Accepting $D$ would allow the term $(\lambda x.\, x\, x)(\lambda x.\, x\, x)$ of the untyped lambda calculus to be encoded, which gives a term of type $D$ with no normal form. A similar type with a constructor $(T \to \bot) \to T$, where $\bot$ is the empty type, would give a closed term of $\bot$, that is, a proof of falsity.

Other standard examples are lists, with $\mathsf{nil}$ and $\mathsf{cons}$, and binary trees. Inductive families, such as vectors of a given length, allow the constructors to target different instances $T(a)$ of a type family.