inductive types. In accordance with the terminology from [@BlanquiJounnaudOkada2002], an inductive type is basic if its constructors have no functional arguments. This class of inductive types includes most simple commonly used inductive types, e.g. natural numbers, lists, finite trees.

In our approach the types of constructors are encoded in the syntactic form of the inductive type. For instance, if $\iota_0, \iota_1 \in
{\ensuremath{{\cal T}}}_I$, then $\iota = \mu(\langle \rangle, \langle \iota_0, \iota_1,
\star, \star \rangle)$ is an inductive type with constructors: $c_1^\iota : \iota$ and $c_2^\iota : \iota_0 \to \iota_1 \to \iota \to
\iota \to \iota$.

If $c_i^\iota \in {\ensuremath{{\cal C}}}$ of arity $n_i$ has signature $\langle
  \iota_1,\ldots,\iota_{n_i} \rangle$ then ${\ensuremath{\vdash}}_{{\ensuremath{{\cal I}}}_s} c_i^\iota :
  \iota_1^* \to \ldots \to \iota_{n_i}^* \to \iota$.

${\ensuremath{\vdash}}_{{\ensuremath{{\cal I}}}_s} o_i^\iota : \iota \to {\ensuremath{\mathrm{Prop}}}$ and ${\ensuremath{\vdash}}_{{\ensuremath{{\cal I}}}_s}
  \forall x : \iota \,.\, o_i^\iota x \supset (d_{i,j}^\iota x :
  \iota_{i,j}^*)$

\[lem\_ind\_leibniz\_implies\_eq\] If $\iota \in {\ensuremath{{\cal T}}}_I$ then ${\ensuremath{\vdash}}_{{\ensuremath{{\cal I}}}_s} \forall x, y : \iota \,.\,
  x =_\iota y \supset x = y$.

We may define the type of natural numbers by ${\ensuremath{\mathrm{Nat}}}\equiv \mu(\langle
\rangle, \langle \star \rangle)$. We use the abbreviations: $0 \equiv
c_1^{\ensuremath{\mathrm{Nat}}}$ (zero), ${\ensuremath{\mathfrak{0}}}\equiv o_1^{\ensuremath{\mathrm{Nat}}}$ (test for zero), ${\ensuremath{\mathfrak{s}}}\equiv c_2^{\ensuremath{\mathrm{Nat}}}$ (successor) and ${\ensuremath{\mathfrak{p}}}\equiv \lambda x 