Dissertation: Higher Inductive Types, Inductive Families, and Inductive-Inductive Types

Martin-Löf type theory is a formal language which is used both as a foun-dation for mathematics and the theoretical basis of a range of functionalprogramming languages. Inductive types are an important part of typetheory which is necessary to express data types by giving a list of rulesstating how to form this data. In this thesis we we tackle several questionsabout different classes of inductive types.In the setting of homotopy type theory, we will take a look at higher in-ductive types based on homotopy coequalizers and characterize their pathspaces with a recursive rule which looks like an induction principle. Thisencapsulates a proof technique known as "encode-decode method".In an extensional meta-theory we will then explore the phenomenonof induction-induction, specify inductice families and discuss how we canreduce each instance of an inductive-inductive type to an inductive family.Our result suggests a way to show that each type theory which encom-passes inductive families can also express all inductive-inductive types.