Higher inductive types, inductive families, and inductive-inductive types
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...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2020
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/60036/ |
| _version_ | 1848799715716497408 |
|---|---|
| author | von Raumer, Jakob |
| author_facet | von Raumer, Jakob |
| author_sort | von Raumer, Jakob |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T20:40:04Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-60036 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T20:40:04Z |
| publishDate | 2020 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-600362025-02-28T12:18:54Z https://eprints.nottingham.ac.uk/60036/ Higher inductive types, inductive families, and inductive-inductive types von Raumer, Jakob 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. 2020-07-24 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en arr https://eprints.nottingham.ac.uk/60036/1/main.pdf von Raumer, Jakob (2020) Higher inductive types, inductive families, and inductive-inductive types. PhD thesis, University of Nottingham. Homotopy type theory Basic type theory Higher inductive types Inductive-inductive types. |
| spellingShingle | Homotopy type theory Basic type theory Higher inductive types Inductive-inductive types. von Raumer, Jakob Higher inductive types, inductive families, and inductive-inductive types |
| title | Higher inductive types, inductive families, and inductive-inductive types |
| title_full | Higher inductive types, inductive families, and inductive-inductive types |
| title_fullStr | Higher inductive types, inductive families, and inductive-inductive types |
| title_full_unstemmed | Higher inductive types, inductive families, and inductive-inductive types |
| title_short | Higher inductive types, inductive families, and inductive-inductive types |
| title_sort | higher inductive types, inductive families, and inductive-inductive types |
| topic | Homotopy type theory Basic type theory Higher inductive types Inductive-inductive types. |
| url | https://eprints.nottingham.ac.uk/60036/ |