Higher Inductive Types Via Impredicative Encodings
Stefano Volpe

Abstract:
In dependent type theory with an impredicative universe, the usual encodings for inductive types borrowed from System F do not satisfy the dependent elimination rule (equivalently, no form of the η-rule holds). Two refinements of these encodings have been proposed to remedy this. Both apply to all W-types. The first is by S. Awodey, J. Frey, and S. Speight. They manage to recover dependent elimination into 0-types of the impredicative universe by assuming the existence of Σ-types, identity types, and function extensionality. By also assuming the existence of a natural numbers type, X. Ripoll Echeveste, inspired by the ideas of M. Shulman, devises a second, distinct refinement for W-types. This time, dependent elimination is possible into the entire impredicative universe.

In this thesis, we show how both encodings can be extended to higher inductive types. While W-types are a popular choice for a working definition of “inductive types”, there are multiple competing definitions of “higher inductive types” in the literature. We test our generalisation of the first refinement on the class of higher inductive types defined by H. Basold, H. Geuvers, and N. van der Weide, and our generalisation of the second on the W-suspensions by K. Sojakova. Finally, we fully formalise the first refined encoding of higher inductive types in the Agda proof assistant.