Impredicative Encodings of Inductive and Coinductive Types

In the impredicative type theory of System F (λ2), it is possible to create inductive data types, such as natural numbers and lists. It is also possible to create coinductive data types such as streams. They work well in the sense that their (co)recursion principles obey the expected computation rules (the \b{eta}-rules). Unfortunately, they do not yield a (co)induction principle, because the necessary uniqueness principles are missing (the η-rules). Awodey, Frey, and Speight (2018) used an extension of λC with sigma-types, equality-types, and functional extensionality to provide System F style inductive types with an induction principle by encoding them as a well-chosen subtype, making them initial algebras. In this thesis, we extend their results. We create a list and quotient type that have the desired induction principles. We show that we can use the technique for general inductive types by defining W-types with an induction principle. We also take the dual notion of their technique and create a coinductive stream type with the desired coinduction principle (also called bisimulation). We finish by showing that this dual approach can be extended to M-types, the generic notion of coinductive types, and the dual of W-types.