Impredicative Encodings of (Higher) Inductive Types
Steve Awodey, Jonas Frey, Sam Speight
TL;DR
The work addresses the problem that System F–style impredicative encodings of inductive types fail to satisfy η-rules and dependent elimination in dependent type theory. It develops a inside-type-theory refinement, inspired by HoTT, that sharpens encodings so η-equivalences become provable and dependent eliminators exist, and then extends the approach to some higher inductive types such as 1-truncation and S^1. Central contributions include a naturality-based refinement for sums, an initial-algebra construction for endofunctors in the impredicative setting, and a concrete 1-type HIT encoding with coherent naturality data. The results yield a coherent framework for impredicative encodings of 0- and 1-types, with implications for W-types, truncations, and HITs, and open directions for semantics, large-elimination, and formalization in proof assistants. The work advances the practical viability of impredicative encodings in dependent type theory and informs ongoing developments in HoTT-inspired type-theoretic foundations.
Abstract
Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.