Quotient inductive-inductive definitions
In this thesis we present a theory of quotient inductive-inductive definitions, which are inductive-inductive definitions extended with constructors for equations. The resulting theory is an improvement over previous treatments of inductive-inductive and indexed inductive definitions in that it unif...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2017
|
| Online Access: | https://eprints.nottingham.ac.uk/42317/ |
| _version_ | 1848796460975390720 |
|---|---|
| author | Dijkstra, Gabe |
| author_facet | Dijkstra, Gabe |
| author_sort | Dijkstra, Gabe |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | In this thesis we present a theory of quotient inductive-inductive definitions, which are inductive-inductive definitions extended with constructors for equations. The resulting theory is an improvement over previous treatments of inductive-inductive and indexed inductive definitions in that it unifies and generalises these into a single framework. The framework can also be seen as a first approximation towards a theory of higher inductive types, but done in a set truncated setting.
We give the type of specifications of quotient inductive-inductive definitions mutually with its interpretation as categories of algebras. A categorical characterisation of the induction principle is given and is shown to coincide with the property of being an initial object in the categories of algebras. From the categorical characterisation of induction, we derive a more type theoretic induction principle for our quotient inductive-inductive definitions that looks like the usual induction principles.
The existence of initial objects in the categories of algebras associated to quotient inductive-inductive definitions is established for a class of definitions. This is done by a colimit construction that can be carried out in type theory itself in the presence of natural numbers, sum types and quotients or equivalently, coequalisers. |
| first_indexed | 2025-11-14T19:48:21Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-42317 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T19:48:21Z |
| publishDate | 2017 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-423172017-12-14T16:01:01Z https://eprints.nottingham.ac.uk/42317/ Quotient inductive-inductive definitions Dijkstra, Gabe In this thesis we present a theory of quotient inductive-inductive definitions, which are inductive-inductive definitions extended with constructors for equations. The resulting theory is an improvement over previous treatments of inductive-inductive and indexed inductive definitions in that it unifies and generalises these into a single framework. The framework can also be seen as a first approximation towards a theory of higher inductive types, but done in a set truncated setting. We give the type of specifications of quotient inductive-inductive definitions mutually with its interpretation as categories of algebras. A categorical characterisation of the induction principle is given and is shown to coincide with the property of being an initial object in the categories of algebras. From the categorical characterisation of induction, we derive a more type theoretic induction principle for our quotient inductive-inductive definitions that looks like the usual induction principles. The existence of initial objects in the categories of algebras associated to quotient inductive-inductive definitions is established for a class of definitions. This is done by a colimit construction that can be carried out in type theory itself in the presence of natural numbers, sum types and quotients or equivalently, coequalisers. 2017-12-14 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en cc_by https://eprints.nottingham.ac.uk/42317/1/thesis.pdf Dijkstra, Gabe (2017) Quotient inductive-inductive definitions. PhD thesis, University of Nottingham. |
| spellingShingle | Dijkstra, Gabe Quotient inductive-inductive definitions |
| title | Quotient inductive-inductive definitions |
| title_full | Quotient inductive-inductive definitions |
| title_fullStr | Quotient inductive-inductive definitions |
| title_full_unstemmed | Quotient inductive-inductive definitions |
| title_short | Quotient inductive-inductive definitions |
| title_sort | quotient inductive-inductive definitions |
| url | https://eprints.nottingham.ac.uk/42317/ |