  We present new induction principles for the syntax of dependent type
theories. These induction principles are expressed in the internal language of
presheaf categories. This ensures for free that any construction is stable
under substitution. In order to combine the internal languages of multiple
presheaf categories, we use Dependent Right Adjoints and Multimodal Type
Theory. Categorical gluing is used to prove these induction principles, but it
not visible in their statements, which involve a notion of model without
context extensions. We illustrate the derivation of these induction principles
by the example of type theory with a hierarchy of universes closed under
function space and natural numbers, but we expect that our method can be
applied to any syntax with bindings. As example applications of these induction
principles, we give short and boilerplate-free proofs of canonicity and
normalization for our example type theory.
