Higher inductive types, inductive families, and inductive-inductive types
Publication Date
July 24, 2020
Creator
Abstract
Martin-Löf type theory is a formal language which is used both as a foundation for mathematics and the theoretical basis of a range of functional programming languages. Inductive types are an important part of type theory which is necessary to express data types by giving a list of rules stating how to form this data. In this thesis we we tackle several questions about different classes of inductive types.
In the setting of homotopy type theory, we will take a look at higher inductive types based on homotopy coequalizers and characterize their path spaces with a recursive rule which looks like an induction principle. This encapsulates a proof technique known as ``encode-decode method''.
In an extensional meta-theory we will then explore the phenomenon of induction-induction, specify inductice families and discuss how we can reduce each instance of an inductive-inductive type to an inductive family. Our result suggests a way to show that each type theory which encompasses inductive families can also express all inductive-inductive types.
Item Type
ethesis
Thesis Type
PhD
Supervisors
Subjects (LC)
Associated Schools / Departments
School of Computer Science (UK)
eprints ID
60036
UoN Repository URI
Except where otherwise noted, this item's license is described as
File(s)![Thumbnail Image]()
Name
main.pdf
Type
Full-text
Description
Examined
Size
600.38 KB
Format
Adobe PDF
Checksum (MD5)
5057562930092d2ede6eceba13aa8795