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/ |