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/ |
| Summary: | 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 defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates. |
|---|