Rafaël Bocquet

Relative induction principles for type theories

2021 · arXiv (Cornell University)

We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a functor F into the syntax is stable over …