  The term UniMath refers both to a formal system for mathematics, as well as a
computer-checked library of mathematics formalized in that system. The UniMath
system is a core dependent type theory, augmented by the univalence axiom. The
system is kept as small as possible in order to ease verification of it - in
particular, general inductive types are not part of the system.
  In this work, we partially remedy the lack of inductive types by constructing
some datatypes and their associated induction principles from other type
constructors. This involves a formalization of a category-theoretic result on
the construction of initial algebras, as well as a mechanism to conveniently
use the datatypes obtained. We also connect this construction to a previous
formalization of substitution for languages with variable binding. Altogether,
we construct a framework that allows us to concisely specify, via a simple
notion of binding signature, a language with variable binding. From such a
specification we obtain the datatype of terms of that language, equipped with a
certified monadic substitution operation and a suitable recursion scheme. Using
this we formalize the untyped lambda calculus and the raw syntax of
Martin-L\"of type theory.
