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