Alternative Impredicative Encodings of Inductive Types
Xavier Ripoll Echeveste

Abstract:
Intensional dependent type theories with an impredicative universe admit an encoding of inductive types similar to the one developed for System F. This technique suffers from one fatal flaw: its recursion principle (non-dependent elimination) does not satisfy the propositional η-rule. Equivalently, it does not have an induction principle (dependent elimination). Awodey, Frey, and Speight (2018) make a proposal to construct inductive types using an impredicative universe by taking the subset of the System F definition satisfying a property named naturality, expanding the theory with Σ-types, identity types, and function extensionality. There is a catch: it can only eliminate into 0-types inside the impredicative universe. In this thesis, we introduce the alternative notion of inductivity. We first prove that it is as strong as naturality—by constructing coproducts and then W-types with their full elimination principles with respect to sets. Later on, we consider Shulman’s claim (2018) that one can lift the h-level restriction by using an intermediate result of his own and including natural numbers in the system. We adapt inductivity (by applying multiple layers thereof) and manage to allow elimination to arbitrary types in the universe, again for coproducts and W-types. Finally, we start studying a categorical generalization of this problem, namely finding the initial algebra of an endofunctor of the impredicative universe, by means of introducing one last property—initiality.