Type theory in type theory using quotient inductive types
We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids referring to preterms or a typability relation but...
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
ACM
2016
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/31169/ |