In algebraic approaches to the syntax and semantics of dependent type theory, the syntax is characterized as the initial object of a category of models. Then the universal property of the initial model corresponds to an induction principle over the syntax: properties of the syntax (canonicity, normalization, etc.) are proven through interpretation of the syntax into various models.

The proofs of many properties do not immediately follow from the induction principle, but require a suitable strengthening of the induction hypotheses. This is typically achieved using methods such as categorical gluing. However, constructing the corresponding model fully explicitly would be tedious, due for instance to the need to check many naturality conditions.

I will present "relative induction principles", which are stronger induction principles that can be used to more directly prove the desired properties of the syntax.

This is based on the paper "For the Metatheory of Type Theory, Internal Sconing is Enough" (joint work with Ambrus Kaposi and Christian Sattler), and on my upcoming PhD thesis "Relative Induction Principles for Second-Order Generalized Algebraic Theories".