Abstract

In the study of type theory, we are often interested in finding ways to reduce a certain class of inductive types to another, possibly simpler class. One reason is that these reductions are semantic constructions, so they further our understanding of the class of types that is being reduced. A more practical reason is that from such reductions we can often derive ways to extend the capabilities of existing proof-assistants based on type theory beyond their original design.

Inductive-inductive types (IITs) are a prime example, since widely-used proof assistants like Coq and Lean do not directly support them. We know that finitary induction-induction can be reduced to inductive families (Kaposi et al.), which means that these proof-assistants could be extended to support finitary IITs (for example, via metaprogramming) without the need to change the core type theory.

Finitary IITs are a rich subclass of induction-induction, however there are interesting IITs that are not finitary. Unfortunately, the currently known method to encode finitary IITs via inductive families cannot be applied to infinitary types, unless the type theory supports function extensionality. However, most proof-assistants based on intensional type theory do not support it. In this talk we present work towards a reduction method for a wide class of infinitary IITs that does not require function extensionality, but instead relies on the presence of a universe of strict propositions, a feature that is now available in many proof-assistants.