Type theory in a type theory with quotient inductive types
Type theory (with dependent types) was introduced by Per Martin-Löf with the intention of providing a foundation for constructive mathematics. A part of constructive mathematics is type theory itself, hence we should be able to say what type theory is using the formal language of type theory. In add...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2017
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/41385/ |
| _version_ | 1848796262908821504 |
|---|---|
| author | Kaposi, Ambrus |
| author_facet | Kaposi, Ambrus |
| author_sort | Kaposi, Ambrus |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Type theory (with dependent types) was introduced by Per Martin-Löf with the intention of providing a foundation for constructive mathematics. A part of constructive mathematics is type theory itself, hence we should be able to say what type theory is using the formal language of type theory. In addition, metatheoretic properties of type theory such as normalisation should be provable in type theory.
The usual way of defining type theory formally is by starting with an inductive definition of precontexts, pretypes and preterms and as a second step defining a ternary typing relation over these three components. Well-typed terms are those preterms for which there exists a precontext and pretype such that the relation holds. However, if we use the rich metalanguage of type theory to talk about type theory, we can define well-typed terms directly as an inductive family indexed over contexts and types. We believe that this latter approach is closer to the spirit of type theory where objects come intrinsically with their types.
Internalising a type theory with dependent types is challenging because of the mutual definitions of types, terms, substitution of terms and the conversion relation. We use induction induction to express this mutual dependency. Furthermore, to reduce the type-theoretic boilerplate needed for reasoning in the syntax, we encode the conversion relation as the equality type of the syntax. We use equality constructors thus we define the syntax as a quotient inductive type (a special case of higher inductive types from homotopy type theory). We define the syntax of a basic type theory with dependent function space, a base type and a family over the base type as a quotient inductive inductive type.
The definition of the syntax comes with a notion of model and an eliminator: whenever one is able to define a model, the eliminator provides a function from the syntax to the model.
We show that this method of representing type theory is practically feasible by defining a number of models: the standard model, the logical predicate interpretation for parametricity (as a syntactic translation) and the proof-relevant presheaf logical predicate interpretation. By extending the latter with a quote function back into the syntax, we prove normalisation for type theory. This can be seen as a proof of normalisation by evaluation.
Internalising the syntax of type theory is not only of theoretical interest. It opens the possibility of type-theoretic metaprogramming in a type-safe way. This could be used for generic programming in type theory and to implement extensions of type theory which are justified by models such as guarded type theory or homotopy type theory. |
| first_indexed | 2025-11-14T19:45:12Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-41385 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T19:45:12Z |
| publishDate | 2017 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-413852017-10-13T01:25:03Z https://eprints.nottingham.ac.uk/41385/ Type theory in a type theory with quotient inductive types Kaposi, Ambrus Type theory (with dependent types) was introduced by Per Martin-Löf with the intention of providing a foundation for constructive mathematics. A part of constructive mathematics is type theory itself, hence we should be able to say what type theory is using the formal language of type theory. In addition, metatheoretic properties of type theory such as normalisation should be provable in type theory. The usual way of defining type theory formally is by starting with an inductive definition of precontexts, pretypes and preterms and as a second step defining a ternary typing relation over these three components. Well-typed terms are those preterms for which there exists a precontext and pretype such that the relation holds. However, if we use the rich metalanguage of type theory to talk about type theory, we can define well-typed terms directly as an inductive family indexed over contexts and types. We believe that this latter approach is closer to the spirit of type theory where objects come intrinsically with their types. Internalising a type theory with dependent types is challenging because of the mutual definitions of types, terms, substitution of terms and the conversion relation. We use induction induction to express this mutual dependency. Furthermore, to reduce the type-theoretic boilerplate needed for reasoning in the syntax, we encode the conversion relation as the equality type of the syntax. We use equality constructors thus we define the syntax as a quotient inductive type (a special case of higher inductive types from homotopy type theory). We define the syntax of a basic type theory with dependent function space, a base type and a family over the base type as a quotient inductive inductive type. The definition of the syntax comes with a notion of model and an eliminator: whenever one is able to define a model, the eliminator provides a function from the syntax to the model. We show that this method of representing type theory is practically feasible by defining a number of models: the standard model, the logical predicate interpretation for parametricity (as a syntactic translation) and the proof-relevant presheaf logical predicate interpretation. By extending the latter with a quote function back into the syntax, we prove normalisation for type theory. This can be seen as a proof of normalisation by evaluation. Internalising the syntax of type theory is not only of theoretical interest. It opens the possibility of type-theoretic metaprogramming in a type-safe way. This could be used for generic programming in type theory and to implement extensions of type theory which are justified by models such as guarded type theory or homotopy type theory. 2017-03-19 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en cc_by https://eprints.nottingham.ac.uk/41385/1/th.pdf Kaposi, Ambrus (2017) Type theory in a type theory with quotient inductive types. PhD thesis, University of Nottingham. type theory homotopy type theory parametricity normalisation by evaluation |
| spellingShingle | type theory homotopy type theory parametricity normalisation by evaluation Kaposi, Ambrus Type theory in a type theory with quotient inductive types |
| title | Type theory in a type theory with quotient inductive types |
| title_full | Type theory in a type theory with quotient inductive types |
| title_fullStr | Type theory in a type theory with quotient inductive types |
| title_full_unstemmed | Type theory in a type theory with quotient inductive types |
| title_short | Type theory in a type theory with quotient inductive types |
| title_sort | type theory in a type theory with quotient inductive types |
| topic | type theory homotopy type theory parametricity normalisation by evaluation |
| url | https://eprints.nottingham.ac.uk/41385/ |